Proof that the intersection of a set is a subset of every member of the set

----> UNIT CONFLICT at   0.25 sec ----> 146 [binary,144.1,19.1] $F.

Length of proof is 4.  Level of proof is 3.

Proof

2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
19 [reference] p2!=p1.
54 [reference] kintersection xf y x=p2|xf z !=p1|z x =p1.
61 [reference] subset x=p1|p1 x notsub(p1 x,p2 x) =p1.
62 [reference] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1.
65 [assumption to refute] subset pair(kintersection bad1 bad2,bad3)!=p1.
66 [assumption to refute] bad1 bad3=p1.
67 [ur,65,62,demod,3,2,3] bad3 notsub(kintersection bad1 bad2,bad3)!=p1.
68 [ur,65,61,demod,2,2,3] kintersection bad1 bad2 notsub(kintersection bad1 bad2,bad3)=p1.
129,128 [ur,67,54,66] kintersection bad1 x notsub(kintersection bad1 bad2,bad3)=p2.
144 [back_demod,68,demod,129] p2=p1.
146 [binary,144.1,19.1] $F.