:: MEMBERED semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"complex-membered"::: means :: MEMBERED:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v1_xcmplx_0 :::"complex"::: ) )); attr "X" is :::"ext-real-membered"::: means :: MEMBERED:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v1_xxreal_0 :::"ext-real"::: ) )); attr "X" is :::"real-membered"::: means :: MEMBERED:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v1_xreal_0 :::"real"::: ) )); attr "X" is :::"rational-membered"::: means :: MEMBERED:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v1_rat_1 :::"rational"::: ) )); attr "X" is :::"integer-membered"::: means :: MEMBERED:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v1_int_1 :::"integer"::: ) )); attr "X" is :::"natural-membered"::: means :: MEMBERED:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v7_ordinal1 :::"natural"::: ) )); end; :: deftheorem defines :::"complex-membered"::: MEMBERED:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_membered :::"complex-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_xcmplx_0 :::"complex"::: ) )) ")" )); :: deftheorem defines :::"ext-real-membered"::: MEMBERED:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_membered :::"ext-real-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_xxreal_0 :::"ext-real"::: ) )) ")" )); :: deftheorem defines :::"real-membered"::: MEMBERED:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_membered :::"real-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_xreal_0 :::"real"::: ) )) ")" )); :: deftheorem defines :::"rational-membered"::: MEMBERED:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_membered :::"rational-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_rat_1 :::"rational"::: ) )) ")" )); :: deftheorem defines :::"integer-membered"::: MEMBERED:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_membered :::"integer-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_int_1 :::"integer"::: ) )) ")" )); :: deftheorem defines :::"natural-membered"::: MEMBERED:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_membered :::"natural-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v7_ordinal1 :::"natural"::: ) )) ")" )); registration cluster ($#v6_membered :::"natural-membered"::: ) -> ($#v5_membered :::"integer-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v5_membered :::"integer-membered"::: ) -> ($#v4_membered :::"rational-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v4_membered :::"rational-membered"::: ) -> ($#v3_membered :::"real-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v3_membered :::"real-membered"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v3_membered :::"real-membered"::: ) -> ($#v1_membered :::"complex-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster -> ($#v1_membered :::"complex-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k2_numbers :::"COMPLEX"::: ) ))); cluster -> ($#v2_membered :::"ext-real-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k7_numbers :::"ExtREAL"::: ) ))); cluster -> ($#v3_membered :::"real-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ))); cluster -> ($#v4_membered :::"rational-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k3_numbers :::"RAT"::: ) ))); cluster -> ($#v5_membered :::"integer-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k4_numbers :::"INT"::: ) ))); cluster -> ($#v6_membered :::"natural-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ))); end; registration cluster (Set ($#k2_numbers :::"COMPLEX"::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ; cluster (Set ($#k7_numbers :::"ExtREAL"::: ) ) -> ($#v2_membered :::"ext-real-membered"::: ) ; cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#v3_membered :::"real-membered"::: ) ; cluster (Set ($#k3_numbers :::"RAT"::: ) ) -> ($#v4_membered :::"rational-membered"::: ) ; cluster (Set ($#k4_numbers :::"INT"::: ) ) -> ($#v5_membered :::"integer-membered"::: ) ; cluster (Set ($#k4_ordinal1 :::"NAT"::: ) ) -> ($#v6_membered :::"natural-membered"::: ) ; end; theorem :: MEMBERED:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_membered :::"complex-membered"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) ; theorem :: MEMBERED:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_membered :::"ext-real-membered"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ))) ; theorem :: MEMBERED:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_membered :::"real-membered"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: MEMBERED:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_membered :::"rational-membered"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) ; theorem :: MEMBERED:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v5_membered :::"integer-membered"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: MEMBERED:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v6_membered :::"natural-membered"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; registrationlet "X" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_xcmplx_0 :::"complex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_xxreal_0 :::"ext-real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_xreal_0 :::"real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_rat_1 :::"rational"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_int_1 :::"integer"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v7_ordinal1 :::"natural"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; theorem :: MEMBERED:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: MEMBERED:8 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: MEMBERED:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: MEMBERED:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: MEMBERED:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: MEMBERED:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: MEMBERED:13 (Bool "for" (Set (Var "X")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) ; theorem :: MEMBERED:14 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ))) ; theorem :: MEMBERED:15 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: MEMBERED:16 (Bool "for" (Set (Var "X")) "being" ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) ; theorem :: MEMBERED:17 (Bool "for" (Set (Var "X")) "being" ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: MEMBERED:18 (Bool "for" (Set (Var "X")) "being" ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: MEMBERED:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" ($#v1_membered :::"complex-membered"::: ) ))) ; theorem :: MEMBERED:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" ($#v2_membered :::"ext-real-membered"::: ) ))) ; theorem :: MEMBERED:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" ($#v3_membered :::"real-membered"::: ) ))) ; theorem :: MEMBERED:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" ($#v4_membered :::"rational-membered"::: ) ))) ; theorem :: MEMBERED:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" ($#v5_membered :::"integer-membered"::: ) ))) ; theorem :: MEMBERED:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" ($#v6_membered :::"natural-membered"::: ) ))) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v6_membered :::"natural-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "c" ($#k1_tarski :::"}"::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "e" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "e" ($#k1_tarski :::"}"::: ) ) -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "r" ($#k1_tarski :::"}"::: ) ) -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "w" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "w" ($#k1_tarski :::"}"::: ) ) -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "i" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "i" ($#k1_tarski :::"}"::: ) ) -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_tarski :::"{"::: ) "n" ($#k1_tarski :::"}"::: ) ) -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "c1", "c2" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "c1" "," "c2" ($#k2_tarski :::"}"::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "e1", "e2" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "e1" "," "e2" ($#k2_tarski :::"}"::: ) ) -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "r1", "r2" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "r1" "," "r2" ($#k2_tarski :::"}"::: ) ) -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "w1", "w2" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "w1" "," "w2" ($#k2_tarski :::"}"::: ) ) -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "i1", "i2" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "i1" "," "i2" ($#k2_tarski :::"}"::: ) ) -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "n1", "n2" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_tarski :::"{"::: ) "n1" "," "n2" ($#k2_tarski :::"}"::: ) ) -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "c1", "c2", "c3" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "c1" "," "c2" "," "c3" ($#k1_enumset1 :::"}"::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "e1", "e2", "e3" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "e1" "," "e2" "," "e3" ($#k1_enumset1 :::"}"::: ) ) -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "r1", "r2", "r3" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "r1" "," "r2" "," "r3" ($#k1_enumset1 :::"}"::: ) ) -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "w1", "w2", "w3" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "w1" "," "w2" "," "w3" ($#k1_enumset1 :::"}"::: ) ) -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "i1", "i2", "i3" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "i1" "," "i2" "," "i3" ($#k1_enumset1 :::"}"::: ) ) -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "n1", "n2", "n3" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_enumset1 :::"{"::: ) "n1" "," "n2" "," "n3" ($#k1_enumset1 :::"}"::: ) ) -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "X" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_membered :::"complex-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_membered :::"ext-real-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_membered :::"real-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_membered :::"rational-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v5_membered :::"integer-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v6_membered :::"natural-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "X", "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "X", "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "X", "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "X", "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "X", "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "X" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v1_membered :::"complex-membered"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v2_membered :::"ext-real-membered"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v3_membered :::"real-membered"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v4_membered :::"rational-membered"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v5_membered :::"integer-membered"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v6_membered :::"natural-membered"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "X" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "X", "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "X", "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "X", "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "X", "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "X", "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v6_membered :::"natural-membered"::: ) ; end; definitionlet "X" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"c="::: "Y" means :: MEMBERED:def 7 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "Y")); end; :: deftheorem defines :::"c="::: MEMBERED:def 7 : (Bool "for" (Set (Var "X")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))); definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"c="::: "Y" means :: MEMBERED:def 8 (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "Y")); end; :: deftheorem defines :::"c="::: MEMBERED:def 8 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))); definitionlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"c="::: "Y" means :: MEMBERED:def 9 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "Y")); end; :: deftheorem defines :::"c="::: MEMBERED:def 9 : (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))); definitionlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"c="::: "Y" means :: MEMBERED:def 10 (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "Y")); end; :: deftheorem defines :::"c="::: MEMBERED:def 10 : (Bool "for" (Set (Var "X")) "being" ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))); definitionlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"c="::: "Y" means :: MEMBERED:def 11 (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "Y")); end; :: deftheorem defines :::"c="::: MEMBERED:def 11 : (Bool "for" (Set (Var "X")) "being" ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))); definitionlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"c="::: "Y" means :: MEMBERED:def 12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "Y")); end; :: deftheorem defines :::"c="::: MEMBERED:def 12 : (Bool "for" (Set (Var "X")) "being" ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))); definitionlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"="::: "Y" means :: MEMBERED:def 13 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "X") "iff" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"="::: MEMBERED:def 13 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"="::: "Y" means :: MEMBERED:def 14 (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "X") "iff" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"="::: MEMBERED:def 14 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"="::: "Y" means :: MEMBERED:def 15 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X") "iff" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"="::: MEMBERED:def 15 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"="::: "Y" means :: MEMBERED:def 16 (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "X") "iff" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"="::: MEMBERED:def 16 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"="::: "Y" means :: MEMBERED:def 17 (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "X") "iff" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"="::: MEMBERED:def 17 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"="::: "Y" means :: MEMBERED:def 18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "X") "iff" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"="::: MEMBERED:def 18 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"misses"::: "Y" means :: MEMBERED:def 19 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"meets"::: MEMBERED:def 19 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"misses"::: "Y" means :: MEMBERED:def 20 (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"meets"::: MEMBERED:def 20 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"misses"::: "Y" means :: MEMBERED:def 21 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"meets"::: MEMBERED:def 21 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"misses"::: "Y" means :: MEMBERED:def 22 (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"meets"::: MEMBERED:def 22 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"misses"::: "Y" means :: MEMBERED:def 23 (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"meets"::: MEMBERED:def 23 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); definitionlet "X", "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "X" :::"misses"::: "Y" means :: MEMBERED:def 24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "Y") ")" )); end; :: deftheorem defines :::"meets"::: MEMBERED:def 24 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )); theorem :: MEMBERED:25 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v1_membered :::"complex-membered"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "F"))) "is" ($#v1_membered :::"complex-membered"::: ) )) ; theorem :: MEMBERED:26 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v2_membered :::"ext-real-membered"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "F"))) "is" ($#v2_membered :::"ext-real-membered"::: ) )) ; theorem :: MEMBERED:27 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v3_membered :::"real-membered"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "F"))) "is" ($#v3_membered :::"real-membered"::: ) )) ; theorem :: MEMBERED:28 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v4_membered :::"rational-membered"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "F"))) "is" ($#v4_membered :::"rational-membered"::: ) )) ; theorem :: MEMBERED:29 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v5_membered :::"integer-membered"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "F"))) "is" ($#v5_membered :::"integer-membered"::: ) )) ; theorem :: MEMBERED:30 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v6_membered :::"natural-membered"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "F"))) "is" ($#v6_membered :::"natural-membered"::: ) )) ; theorem :: MEMBERED:31 (Bool "for" (Set (Var "F")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "X")) "is" ($#v1_membered :::"complex-membered"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v1_membered :::"complex-membered"::: ) )) ; theorem :: MEMBERED:32 (Bool "for" (Set (Var "F")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "X")) "is" ($#v2_membered :::"ext-real-membered"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v2_membered :::"ext-real-membered"::: ) )) ; theorem :: MEMBERED:33 (Bool "for" (Set (Var "F")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "X")) "is" ($#v3_membered :::"real-membered"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v3_membered :::"real-membered"::: ) )) ; theorem :: MEMBERED:34 (Bool "for" (Set (Var "F")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "X")) "is" ($#v4_membered :::"rational-membered"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v4_membered :::"rational-membered"::: ) )) ; theorem :: MEMBERED:35 (Bool "for" (Set (Var "F")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "X")) "is" ($#v5_membered :::"integer-membered"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v5_membered :::"integer-membered"::: ) )) ; theorem :: MEMBERED:36 (Bool "for" (Set (Var "F")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "X")) "is" ($#v6_membered :::"natural-membered"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v6_membered :::"natural-membered"::: ) )) ; scheme :: MEMBERED:sch 1 CMSeparation{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "c"))]) ")" ))) proof end; scheme :: MEMBERED:sch 2 EMSeparation{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "e")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "e"))]) ")" ))) proof end; scheme :: MEMBERED:sch 3 RMSeparation{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "r"))]) ")" ))) proof end; scheme :: MEMBERED:sch 4 WMSeparation{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "w"))]) ")" ))) proof end; scheme :: MEMBERED:sch 5 IMSeparation{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "i"))]) ")" ))) proof end; scheme :: MEMBERED:sch 6 NMSeparation{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "n"))]) ")" ))) proof end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster -> ($#v6_membered :::"natural-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: MEMBERED:37 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) ")" )) "holds" (Bool "ex" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"add-closed"::: means :: MEMBERED:def 25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) "X")); end; :: deftheorem defines :::"add-closed"::: MEMBERED:def 25 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v7_membered :::"add-closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v7_membered :::"add-closed"::: ) for ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_numbers :::"COMPLEX"::: ) ) -> ($#v7_membered :::"add-closed"::: ) ; cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#v7_membered :::"add-closed"::: ) ; cluster (Set ($#k3_numbers :::"RAT"::: ) ) -> ($#v7_membered :::"add-closed"::: ) ; cluster (Set ($#k4_numbers :::"INT"::: ) ) -> ($#v7_membered :::"add-closed"::: ) ; cluster (Set ($#k4_ordinal1 :::"NAT"::: ) ) -> ($#v7_membered :::"add-closed"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#v7_membered :::"add-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end;