:: SUBSET_1 semantic presentation begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_zfmisc_1 :::"bool"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "x1", "x2", "x3" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" ($#k1_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x4" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" ($#k2_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x5" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" ($#k3_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x6" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" ($#k4_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x7" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" ($#k5_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x8" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8" ($#k6_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x9" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8" "," "x9" ($#k7_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "x10" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8" "," "x9" "," "x10" ($#k8_enumset1 :::"}"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"Element"::: "of" "X" -> ($#m1_hidden :::"set"::: ) means :: SUBSET_1:def 1 (Bool it ($#r2_hidden :::"in"::: ) "X") if (Bool (Bool "not" "X" "is" ($#v1_xboole_0 :::"empty"::: ) )) otherwise (Bool it "is" ($#v1_xboole_0 :::"empty"::: ) ); sethood (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Const "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "ex" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Const "X")))) "holds" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))))) ")" ) "or" (Bool "(" (Bool (Set (Const "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "ex" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))))) ")" ) ")" ) ; end; :: deftheorem defines :::"Element"::: SUBSET_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "b2")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Subset of "X" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "X1", "X2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X1" "," "X2" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X1", "X2", "X3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" ($#k3_zfmisc_1 :::":]"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X1", "X2", "X3", "X4" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" "," "X4" ($#k4_zfmisc_1 :::":]"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; registrationlet "E" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "E"); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; func :::"{}"::: "E" -> ($#m1_subset_1 :::"Subset":::) "of" "E" equals :: SUBSET_1:def 2 (Set ($#k1_xboole_0 :::"{}"::: ) ); func :::"[#]"::: "E" -> ($#m1_subset_1 :::"Subset":::) "of" "E" equals :: SUBSET_1:def 3 "E"; end; :: deftheorem defines :::"{}"::: SUBSET_1:def 2 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_subset_1 :::"{}"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); :: deftheorem defines :::"[#]"::: SUBSET_1:def 3 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Var "E")))); registrationlet "E" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_subset_1 :::"{}"::: ) "E") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: SUBSET_1:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")))) ; theorem :: SUBSET_1:2 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: SUBSET_1:3 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: SUBSET_1:4 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); func "A" :::"`"::: -> ($#m1_subset_1 :::"Subset":::) "of" "E" equals :: SUBSET_1:def 4 (Set "E" ($#k4_xboole_0 :::"\"::: ) "A"); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Const "E")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Const "E")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "b1"))))) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "E"; :: original: :::"\+\"::: redefine func "A" :::"\+\"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "E"; end; :: deftheorem defines :::"`"::: SUBSET_1:def 4 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "A")))))); definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; :: original: :::"\"::: redefine func "X" :::"\"::: "Y" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"\"::: redefine func "A" :::"\"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "E"; end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"/\"::: redefine func "A" :::"/\"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "E"; end; definitionlet "E", "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); :: original: :::"/\"::: redefine func "X" :::"/\"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "E"; end; theorem :: SUBSET_1:5 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))))) ; theorem :: SUBSET_1:6 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")))))) ; theorem :: SUBSET_1:7 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "C")))))) ; theorem :: SUBSET_1:8 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) ")" ) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "C")))))) ; theorem :: SUBSET_1:9 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "E")) ")" ) ($#k3_subset_1 :::"`"::: ) ))) ; theorem :: SUBSET_1:10 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")))))) ; theorem :: SUBSET_1:11 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")))))) ; theorem :: SUBSET_1:12 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) ")" ))) ; theorem :: SUBSET_1:13 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ))))) ; theorem :: SUBSET_1:14 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))))) ; theorem :: SUBSET_1:15 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: SUBSET_1:16 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:17 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; theorem :: SUBSET_1:18 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_subset_1 :::"{}"::: ) (Set (Var "E")))) ")" ))) ; theorem :: SUBSET_1:19 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")))) ")" ))) ; theorem :: SUBSET_1:20 (Bool "for" (Set (Var "E")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: SUBSET_1:21 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:22 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:23 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )) ")" ))) ; theorem :: SUBSET_1:24 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ))) ; theorem :: SUBSET_1:25 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:26 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:27 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: SUBSET_1:28 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: SUBSET_1:29 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: SUBSET_1:30 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:31 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:32 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SUBSET_1:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: SUBSET_1:41 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")))) ; scheme :: SUBSET_1:sch 1 SubsetEx{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))]) ")" ) ")" ))) proof end; scheme :: SUBSET_1:sch 2 SubsetEq{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) provided (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) "iff" (Bool P1[(Set (Var "y"))]) ")" )) and (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "iff" (Bool P1[(Set (Var "y"))]) ")" )) proof end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"misses"::: redefine pred "X" :::"misses"::: "Y"; irreflexivity (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool bbbadR1_XBOOLE_0((Set (Var "b1")) "," (Set (Var "b1"))))) ; end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"misses"::: redefine pred "X" :::"meets"::: "Y"; reflexivity (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool bbbadR1_XBOOLE_0((Set (Var "b1")) "," (Set (Var "b1"))))) ; end; definitionlet "S" be ($#m1_hidden :::"set"::: ) ; func :::"choose"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" "S" equals :: SUBSET_1:def 5 "the" ($#m1_subset_1 :::"Element"::: ) "of" "S"; end; :: deftheorem defines :::"choose"::: SUBSET_1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_subset_1 :::"choose"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")))); begin scheme :: SUBSET_1:sch 3 SubsetEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "iff" (Bool P1[(Set (Var "x"))]) ")" ))) proof end; scheme :: SUBSET_1:sch 4 SubComp{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) provided (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) "iff" (Bool P1[(Set (Var "X"))]) ")" )) and (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "iff" (Bool P1[(Set (Var "X"))]) ")" )) proof end; theorem :: SUBSET_1:42 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); attr "A" is :::"proper"::: means :: SUBSET_1:def 6 (Bool "A" ($#r1_hidden :::"<>"::: ) "E"); end; :: deftheorem defines :::"proper"::: SUBSET_1:def 6 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_subset_1 :::"proper"::: ) ) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) ")" ))); registrationlet "E" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_subset_1 :::"[#]"::: ) "E") -> ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ; end; registrationlet "E" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "E"); end; registrationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "E"); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_subset_1 :::"proper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "E"); end; registrationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_subset_1 :::"proper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "E"); end; registrationlet "E" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "E"); end; theorem :: SUBSET_1:43 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "A")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X"))(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: SUBSET_1:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) ))) ")" )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; redefine attr "X" is :::"trivial"::: means :: SUBSET_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"trivial"::: SUBSET_1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "X" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_zfmisc_1 :::"trivial"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "X" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; theorem :: SUBSET_1:45 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "st" (Bool (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) "holds" (Bool "ex" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Var "d1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "d2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "d1")) ($#r1_hidden :::"<>"::: ) (Set (Var "d2"))) ")" )))) ; theorem :: SUBSET_1:46 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: SUBSET_1:47 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: SUBSET_1:48 (Bool "for" (Set (Var "X")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" )))) ;