Proof of alternate defining property for subset

----> UNIT CONFLICT at   0.20 sec ----> 101 [binary,99.1,60.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference] pair(p1 x,p2 x)=x.
57 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
60 [assumption to refute] subset bad!=p2.
61 [assumption to refute] p1 bad badc=p1.
62 [assumption to refute] p2 bad badc!=p1.
99 [ur,62,57,61,demod,5] subset bad=p2.
101 [binary,99.1,60.1] $F.



up show outline