Proof of pushset Lemma 1

-----> EMPTY CLAUSE at 1054.09 sec ----> 14795 [para_into,14793.1.1,50.1.1,unit_del,22,14794] $F.

Length of proof is 5.  Level of proof is 5.

Proof

2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
22 [reference] p1!=p2.
50 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
51 [reference] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1.
64 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
76 [reference] subset pair(xs,closure pair(xs,xf))=p1.
79 [reference] closure x y=p1|closure x y =p2.
82 [reference] closedunder pair(x2,p2 x1)=p2|subset pair(p1 x1,x2) =p2|subset pair(closure x1,x2) =p1.
95 [reference] closure pair(notp1 charq,setof) (push x)=closure pair(notp1 charq,setof) x.
101 [assumption to refute] closure pair(notp1 charq,push) bad!=p2.
102 [assumption to refute] closure pair(notp1 charq,setof) bad!=p1.
105 [ur,101,79] closure pair(notp1 charq,push) bad=p1.
148 [ur,105,64,102] subset pair(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))=p2.
677 [para_into,148.1.1,82.3.1,demod,3,2,unit_del,22] closedunder pair(closure pair(notp1 charq,setof),push)=p2|subset pair(notp1 charq,closure pair(notp1 charq,setof)) =p2.
14793 [para_into,677.2.1,76.1.1,unit_del,22] closedunder pair(closure pair(notp1 charq,setof),push)=p2.
14794 [para_into,14793.1.1,51.1.1,demod,95,unit_del,22] closure pair(notp1 charq,setof) notclosed(closure pair(notp1 charq,setof),push)!=p1.
14795 [para_into,14793.1.1,50.1.1,unit_del,22,14794] $F.