pm5.61 Show Code edit
# Theorem *5.61 of [bib/WhiteheadRussell] p. 125.
## Eliminate Disjoint
thm (pm5.61 () () (<-> (/\ (\/ ph ps) (-. ps)) (/\ ph (-. ps))) ps ph orel2 imdistanri ph ps orc (-. ps) anim1i impbii)
(<-> (/\ (\/ ph ps) (-. ps)) (/\ ph (-. ps)))
edit