:: DOMAIN_1 semantic presentation begin theorem :: DOMAIN_1:1 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: DOMAIN_1:2 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; definitionlet "X1", "X2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X1")); let "x2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X2")); :: original: :::"["::: redefine func :::"[":::"x1" "," "x2":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X1" "," "X2" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "X1", "X2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X1")) "," (Set (Const "X2")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X1"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X2"; end; theorem :: DOMAIN_1:3 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2"))(Bool "ex" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))))) ")" ))) ; theorem :: DOMAIN_1:4 (Bool "for" (Set (Var "D")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2"))(Bool "ex" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))))) ")" ) ")" )) "holds" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ))) ; theorem :: DOMAIN_1:5 (Bool "for" (Set (Var "D")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2"))(Bool "ex" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))))) ")" )) ")" )) ; definitionlet "X1", "X2", "X3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X1")); let "x2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X2")); let "x3" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X3")); :: original: :::"["::: redefine func :::"[":::"x1" "," "x2" "," "x3":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" ($#k3_zfmisc_1 :::":]"::: ) ); end; theorem :: DOMAIN_1:6 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))))) ")" )))) ; theorem :: DOMAIN_1:7 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))))) ")" )))) ; theorem :: DOMAIN_1:8 (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "x3")))))) ")" )))) ; theorem :: DOMAIN_1:9 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_mcart_1 :::"`1_3"::: ) )) & (Bool (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_mcart_1 :::"`2_3"::: ) )) & (Bool (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_mcart_1 :::"`3_3"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: DOMAIN_1:10 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2"))(Bool "ex" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3"))(Bool "ex" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )))))) ")" ))) ; theorem :: DOMAIN_1:11 (Bool "for" (Set (Var "D")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2"))(Bool "ex" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3"))(Bool "ex" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )))))) ")" ) ")" )) "holds" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ))) ; theorem :: DOMAIN_1:12 (Bool "for" (Set (Var "D")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2"))(Bool "ex" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3"))(Bool "ex" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )))))) ")" )) ")" )) ; definitionlet "X1", "X2", "X3", "X4" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X1")); let "x2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X2")); let "x3" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X3")); let "x4" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X4")); :: original: :::"["::: redefine func :::"[":::"x1" "," "x2" "," "x3" "," "x4":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" "," "X4" ($#k4_zfmisc_1 :::":]"::: ) ); end; theorem :: DOMAIN_1:13 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))))))) ")" )))) ; theorem :: DOMAIN_1:14 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))))))) ")" )))) ; theorem :: DOMAIN_1:15 (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))))))) ")" )))) ; theorem :: DOMAIN_1:16 (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))))))) ")" )))) ; theorem :: DOMAIN_1:17 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k4_mcart_1 :::"`1_4"::: ) )) & (Bool (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_mcart_1 :::"`2_4"::: ) )) & (Bool (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_mcart_1 :::"`3_4"::: ) )) & (Bool (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k7_mcart_1 :::"`4_4"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; scheme :: DOMAIN_1:sch 1 Fraenkel1{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool P1[(Set (Var "x1"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")))) proof end; scheme :: DOMAIN_1:sch 2 Fraenkel2{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) : (Bool P1[(Set (Var "x1")) "," (Set (Var "x2"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ))) proof end; scheme :: DOMAIN_1:sch 3 Fraenkel3{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "{" (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")), x3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) : (Bool P1[(Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ))) proof end; scheme :: DOMAIN_1:sch 4 Fraenkel4{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "{" (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")), x3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")), x4 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) : (Bool P1[(Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ))) proof end; scheme :: DOMAIN_1:sch 5 Fraenkel5{ P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) "st" (Bool (Bool P1[(Set (Var "x1"))])) "holds" (Bool P2[(Set (Var "x1"))]) ")" )) "holds" (Bool "{" (Set (Var "y1")) where y1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool P1[(Set (Var "y1"))]) "}" ($#r1_tarski :::"c="::: ) "{" (Set (Var "z1")) where z1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool P2[(Set (Var "z1"))]) "}" )) proof end; scheme :: DOMAIN_1:sch 6 Fraenkel6{ P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) "holds" (Bool "(" (Bool P1[(Set (Var "x1"))]) "iff" (Bool P2[(Set (Var "x1"))]) ")" ) ")" )) "holds" (Bool "{" (Set (Var "y1")) where y1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool P1[(Set (Var "y1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set (Var "z1")) where z1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool P2[(Set (Var "z1"))]) "}" )) proof end; scheme :: DOMAIN_1:sch 7 SubsetD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "d"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" )) proof end; theorem :: DOMAIN_1:18 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool verum) "}" )) ; theorem :: DOMAIN_1:19 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) : (Bool verum) "}" )) ; theorem :: DOMAIN_1:20 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")), x3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) : (Bool verum) "}" )) ; theorem :: DOMAIN_1:21 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")), x3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")), x4 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) : (Bool verum) "}" )) ; theorem :: DOMAIN_1:22 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) "}" ))) ; theorem :: DOMAIN_1:23 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "holds" (Bool (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k8_mcart_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) ")" ) "}" )))) ; theorem :: DOMAIN_1:24 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) (Bool "for" (Set (Var "A3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X3")) "holds" (Bool (Set ($#k9_mcart_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) ($#k9_mcart_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")), x3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "A3"))) ")" ) "}" ))))) ; theorem :: DOMAIN_1:25 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) (Bool "for" (Set (Var "A3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X3")) (Bool "for" (Set (Var "A4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X4")) "holds" (Bool (Set ($#k10_mcart_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "A4")) ($#k10_mcart_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) ) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")), x3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")), x4 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "A3"))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set (Var "A4"))) ")" ) "}" )))))) ; theorem :: DOMAIN_1:26 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_subset_1 :::"{}"::: ) (Set (Var "X1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool contradiction) "}" )) ; theorem :: DOMAIN_1:27 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1")))) "}" ))) ; theorem :: DOMAIN_1:28 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) ")" ) "}" ))) ; theorem :: DOMAIN_1:29 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) "or" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) ")" ) "}" ))) ; theorem :: DOMAIN_1:30 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) ")" ) "}" ))) ; theorem :: DOMAIN_1:31 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1")))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) ")" ) ")" ) "}" ))) ; theorem :: DOMAIN_1:32 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1")))) "iff" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) ")" ) "}" ))) ; theorem :: DOMAIN_1:33 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) "iff" (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) ")" ) "}" ))) ; theorem :: DOMAIN_1:34 (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "A1")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x1")) where x1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) : (Bool "(" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) ")" ) "or" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1")))) ")" ) ")" ) "}" ))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x3" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2" "," "x3":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x4" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2" "," "x3" "," "x4":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x5" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x6" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x7" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; let "x8" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"{"::: redefine func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" "D"; end; begin scheme :: DOMAIN_1:sch 8 SubsetFD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F2 "(" ")" )) proof end; scheme :: DOMAIN_1:sch 9 SubsetFD2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F3 "(" ")" )) proof end; definitionlet "D1", "D2", "D3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D1")) "," (Set (Const "D2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "D3")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`11"::: redefine func "x" :::"`11"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "D1"; :: original: :::"`12"::: redefine func "x" :::"`12"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "D2"; end; definitionlet "D1", "D2", "D3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D1")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D2")) "," (Set (Const "D3")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`21"::: redefine func "x" :::"`21"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "D2"; :: original: :::"`22"::: redefine func "x" :::"`22"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "D3"; end; scheme :: DOMAIN_1:sch 10 AndScheme{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "a"))]) ")" ) "}" ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "a1")) where a1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "a1"))]) "}" ($#k3_xboole_0 :::"/\"::: ) "{" (Set (Var "a2")) where a2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P2[(Set (Var "a2"))]) "}" )) proof end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_ordinal1 :::"c=-linear"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "A"); end;