Proof of converse alternate defining property for subset

Proof of converse alternate defining property for `subset`

----> UNIT CONFLICT at  27.39 sec ----> 4732 [binary,4730.1,61.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



5 [reference] pair(p1 x,p2 x)=x.
58 [reference] subset pair(x1,x2)=p1|x1 notsub(x1,x2) =p1.
59 [reference] subset pair(x1,x2)=p1|x2 notsub(x1,x2) !=p1.
61 [assumption to refute] subset bad!=p1.
62 [assumption to refute] p1 bad notsub(p1 bad,p2 bad)!=p1|p2 bad notsub(p1 bad,p2 bad) =p1.
103 [hyper,62,58,demod,5,unit_del,61] p2 bad notsub(p1 bad,p2 bad)=p1.
4730 [hyper,103,59,demod,5] subset bad=p1.
4732 [binary,4730.1,61.1] $F.