:: MEMBER_1 semantic presentation begin definitionlet "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"-"::: redefine func :::"-"::: "w" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"""::: redefine func "w" :::"""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "w1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"*"::: redefine func "w" :::"*"::: "w1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; registrationlet "a", "b", "c", "d" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_enumset1 :::"{"::: ) "a" "," "b" "," "c" "," "d" ($#k2_enumset1 :::"}"::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "a", "b", "c", "d" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_enumset1 :::"{"::: ) "a" "," "b" "," "c" "," "d" ($#k2_enumset1 :::"}"::: ) ) -> ($#v2_membered :::"ext-real-membered"::: ) ; end; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func :::"--"::: "F" -> ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 1 "{" (Set "(" ($#k1_member_1 :::"-"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "F") "}" ; involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_member_1 :::"-"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "}" )) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_member_1 :::"-"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "}" )) ; end; :: deftheorem defines :::"--"::: MEMBER_1:def 1 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_member_1 :::"-"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )); theorem :: MEMBER_1:1 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_member_1 :::"--"::: ) (Set (Var "F")))) ")" ))) ; theorem :: MEMBER_1:2 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_member_1 :::"--"::: ) (Set (Var "F")))) ")" ))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_member_1 :::"--"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_member_1 :::"--"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:3 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) "iff" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_member_1 :::"--"::: ) (Set (Var "G")))) ")" )) ; theorem :: MEMBER_1:4 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_member_1 :::"--"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G")))) ; theorem :: MEMBER_1:5 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "G")) ")" )))) ; theorem :: MEMBER_1:6 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "G")) ")" )))) ; theorem :: MEMBER_1:7 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "G")) ")" )))) ; theorem :: MEMBER_1:8 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "G")) ")" )))) ; theorem :: MEMBER_1:9 (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k2_xxreal_3 :::"-"::: ) (Set (Var "f")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:10 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_xxreal_3 :::"-"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k2_xxreal_3 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; func :::"--"::: "A" -> ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 2 "{" (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "A") "}" ; involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "}" )) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "}" )) ; end; :: deftheorem defines :::"--"::: MEMBER_1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" )); theorem :: MEMBER_1:11 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_member_1 :::"--"::: ) (Set (Var "A")))) ")" ))) ; theorem :: MEMBER_1:12 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k5_member_1 :::"--"::: ) (Set (Var "A")))) ")" ))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_member_1 :::"--"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_member_1 :::"--"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_member_1 :::"--"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_member_1 :::"--"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_member_1 :::"--"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; theorem :: MEMBER_1:13 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set (Var "B")))) ")" )) ; theorem :: MEMBER_1:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) ; theorem :: MEMBER_1:15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:16 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:17 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:19 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "F" :::""""::: -> ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 3 "{" (Set "(" (Set (Var "w")) ($#k2_member_1 :::"""::: ) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "F") "}" ; end; :: deftheorem defines :::""""::: MEMBER_1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k6_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w")) ($#k2_member_1 :::"""::: ) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )); theorem :: MEMBER_1:21 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "f")) ($#k5_xxreal_3 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k6_member_1 :::""""::: ) )))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k6_member_1 :::""""::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k6_member_1 :::""""::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:22 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k6_member_1 :::""""::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k6_member_1 :::""""::: ) ))) ; theorem :: MEMBER_1:23 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "G")) ")" ) ($#k6_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_member_1 :::""""::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k6_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:24 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" ) ($#k6_member_1 :::""""::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_member_1 :::""""::: ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "G")) ($#k6_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:25 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k6_member_1 :::""""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k6_member_1 :::""""::: ) ))) ; theorem :: MEMBER_1:26 (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k6_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k5_xxreal_3 :::"""::: ) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:27 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k6_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k5_xxreal_3 :::"""::: ) ")" ) "," (Set "(" (Set (Var "g")) ($#k5_xxreal_3 :::"""::: ) ")" ) ($#k2_tarski :::"}"::: ) ))) ; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "A" :::""""::: -> ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 4 "{" (Set "(" (Set (Var "c")) ($#k2_binop_2 :::"""::: ) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "A") "}" ; involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c")) ($#k2_binop_2 :::"""::: ) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "}" )) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c")) ($#k2_binop_2 :::"""::: ) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "}" )) ; end; :: deftheorem defines :::""""::: MEMBER_1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c")) ($#k2_binop_2 :::"""::: ) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" )); theorem :: MEMBER_1:28 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Set (Var "a")) ($#k2_binop_2 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_member_1 :::""""::: ) )) ")" ))) ; theorem :: MEMBER_1:29 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_binop_2 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_member_1 :::""""::: ) )) ")" ))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k7_member_1 :::""""::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k7_member_1 :::""""::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k7_member_1 :::""""::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k7_member_1 :::""""::: ) ) -> ($#v1_membered :::"complex-membered"::: ) ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; theorem :: MEMBER_1:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "A")) ($#k7_member_1 :::""""::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k7_member_1 :::""""::: ) )) ")" )) ; theorem :: MEMBER_1:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k7_member_1 :::""""::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) ; theorem :: MEMBER_1:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_member_1 :::""""::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k7_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_member_1 :::""""::: ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k7_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:34 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_member_1 :::""""::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "B")) ($#k7_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_member_1 :::""""::: ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "B")) ($#k7_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:36 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k7_member_1 :::""""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k7_member_1 :::""""::: ) ))) ; theorem :: MEMBER_1:37 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k2_binop_2 :::"""::: ) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:38 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k2_binop_2 :::"""::: ) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_binop_2 :::"""::: ) ")" ) ($#k2_tarski :::"}"::: ) ))) ; definitionlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "F" :::"++"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 5 "{" (Set "(" (Set (Var "w1")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) "G") ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" ))) ; end; :: deftheorem defines :::"++"::: MEMBER_1:def 5 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )); theorem :: MEMBER_1:39 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "G")))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k8_member_1 :::"++"::: ) "G") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "G" ($#k8_member_1 :::"++"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k8_member_1 :::"++"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k8_member_1 :::"++"::: ) "G") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:40 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k8_member_1 :::"++"::: ) (Set (Var "I"))))) ; theorem :: MEMBER_1:41 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set "(" (Set (Var "G")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "G")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:42 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set "(" (Set (Var "G")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "G")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:43 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k8_member_1 :::"++"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "g")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "g")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:44 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k8_member_1 :::"++"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "h")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:45 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k8_member_1 :::"++"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "i")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "A" :::"++"::: "B" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 6 "{" (Set "(" (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" ))) ; end; :: deftheorem defines :::"++"::: MEMBER_1:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )); theorem :: MEMBER_1:46 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "B" ($#k9_member_1 :::"++"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A", "B" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A", "B" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A", "B" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k9_member_1 :::"++"::: ) "B") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; theorem :: MEMBER_1:47 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k9_member_1 :::"++"::: ) (Set (Var "D"))))) ; theorem :: MEMBER_1:48 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:49 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:50 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" ) ($#k9_member_1 :::"++"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "B")) ($#k9_member_1 :::"++"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:51 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k9_member_1 :::"++"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:52 (Bool "for" (Set (Var "a")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k9_member_1 :::"++"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "t")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:53 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k9_member_1 :::"++"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "t")) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_binop_2 :::"+"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_binop_2 :::"+"::: ) (Set (Var "t")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "F" :::"--"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 7 (Set "F" ($#k8_member_1 :::"++"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) "G" ")" )); end; :: deftheorem defines :::"--"::: MEMBER_1:def 7 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "G")) ")" )))); theorem :: MEMBER_1:54 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )) ; theorem :: MEMBER_1:55 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "G")))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k10_member_1 :::"--"::: ) "G") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "G" ($#k10_member_1 :::"--"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k10_member_1 :::"--"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k10_member_1 :::"--"::: ) "G") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:56 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k10_member_1 :::"--"::: ) (Set (Var "I"))))) ; theorem :: MEMBER_1:57 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set "(" (Set (Var "G")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "G")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:58 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set "(" (Set (Var "G")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "G")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:59 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k8_member_1 :::"++"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k10_member_1 :::"--"::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:60 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k8_member_1 :::"++"::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:61 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k10_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "g")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "g")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:62 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k10_member_1 :::"--"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:63 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k10_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "h")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:64 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k10_member_1 :::"--"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "i")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "A" :::"--"::: "B" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 8 (Set "A" ($#k9_member_1 :::"++"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) "B" ")" )); end; :: deftheorem defines :::"--"::: MEMBER_1:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )))); theorem :: MEMBER_1:65 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) ; theorem :: MEMBER_1:66 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k11_member_1 :::"--"::: ) "B") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "B" ($#k11_member_1 :::"--"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k11_member_1 :::"--"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k11_member_1 :::"--"::: ) "B") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k11_member_1 :::"--"::: ) "B") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A", "B" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k11_member_1 :::"--"::: ) "B") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A", "B" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k11_member_1 :::"--"::: ) "B") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; theorem :: MEMBER_1:67 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k11_member_1 :::"--"::: ) (Set (Var "D"))))) ; theorem :: MEMBER_1:68 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:69 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:70 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k11_member_1 :::"--"::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:71 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k9_member_1 :::"++"::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:72 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "B")) ($#k11_member_1 :::"--"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" ) ($#k11_member_1 :::"--"::: ) (Set (Var "C"))))) ; theorem :: MEMBER_1:73 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "B")) ($#k9_member_1 :::"++"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" ) ($#k11_member_1 :::"--"::: ) (Set (Var "C"))))) ; theorem :: MEMBER_1:74 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "B")) ($#k11_member_1 :::"--"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" ) ($#k9_member_1 :::"++"::: ) (Set (Var "C"))))) ; theorem :: MEMBER_1:75 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k11_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:76 (Bool "for" (Set (Var "a")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k11_member_1 :::"--"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:77 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "s")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k11_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "b")) ($#k4_binop_2 :::"-"::: ) (Set (Var "s")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:78 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k11_member_1 :::"--"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")) ")" ) "," (Set "(" (Set (Var "b")) ($#k4_binop_2 :::"-"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "b")) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "F" :::"**"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 9 "{" (Set "(" (Set (Var "w1")) ($#k3_member_1 :::"*"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) "G") ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k3_member_1 :::"*"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k3_member_1 :::"*"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" ))) ; end; :: deftheorem defines :::"**"::: MEMBER_1:def 9 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k3_member_1 :::"*"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )); registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k12_member_1 :::"**"::: ) "G") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "G" ($#k12_member_1 :::"**"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k12_member_1 :::"**"::: ) "G") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:79 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")))))) ; registrationlet "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k12_member_1 :::"**"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MEMBER_1:80 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")) ")" ) ($#k12_member_1 :::"**"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set "(" (Set (Var "G")) ($#k12_member_1 :::"**"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:81 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k12_member_1 :::"**"::: ) (Set (Var "I"))))) ; theorem :: MEMBER_1:82 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set "(" (Set (Var "G")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:83 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set "(" (Set (Var "G")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:84 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set "(" ($#k4_member_1 :::"--"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")) ")" )))) ; theorem :: MEMBER_1:85 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")) ")" ) ($#k6_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_member_1 :::""""::: ) ")" ) ($#k12_member_1 :::"**"::: ) (Set "(" (Set (Var "G")) ($#k6_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:86 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k12_member_1 :::"**"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "g")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "g")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:87 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k12_member_1 :::"**"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:88 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k12_member_1 :::"**"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "i")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "A" :::"**"::: "B" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 10 "{" (Set "(" (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" ))) ; end; :: deftheorem defines :::"**"::: MEMBER_1:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )); theorem :: MEMBER_1:89 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "B" ($#k13_member_1 :::"**"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A", "B" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A", "B" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A", "B" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k13_member_1 :::"**"::: ) "B") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; theorem :: MEMBER_1:90 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k13_member_1 :::"**"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:91 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k13_member_1 :::"**"::: ) (Set (Var "D"))))) ; theorem :: MEMBER_1:92 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:93 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:94 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:95 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k9_member_1 :::"++"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:96 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k11_member_1 :::"--"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:97 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k7_member_1 :::""""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_member_1 :::""""::: ) ")" ) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k7_member_1 :::""""::: ) ")" )))) ; theorem :: MEMBER_1:98 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k13_member_1 :::"**"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:99 (Bool "for" (Set (Var "a")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k13_member_1 :::"**"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "t")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:100 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k13_member_1 :::"**"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "t")) ")" ) "," (Set "(" (Set (Var "b")) ($#k5_binop_2 :::"*"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "b")) ($#k5_binop_2 :::"*"::: ) (Set (Var "t")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "F" :::"///"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 11 (Set "F" ($#k12_member_1 :::"**"::: ) (Set "(" "G" ($#k6_member_1 :::""""::: ) ")" )); end; :: deftheorem defines :::"///"::: MEMBER_1:def 11 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set "(" (Set (Var "G")) ($#k6_member_1 :::""""::: ) ")" )))); theorem :: MEMBER_1:101 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w1")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "w2")) ")" ) where w1, w2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )) ; theorem :: MEMBER_1:102 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G")))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k14_member_1 :::"///"::: ) "G") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "G" ($#k14_member_1 :::"///"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k14_member_1 :::"///"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k14_member_1 :::"///"::: ) "G") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:103 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k14_member_1 :::"///"::: ) (Set (Var "I"))))) ; theorem :: MEMBER_1:104 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "G")) ")" ) ($#k14_member_1 :::"///"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:105 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" ) ($#k14_member_1 :::"///"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "G")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:106 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set "(" (Set (Var "G")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:107 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set "(" (Set (Var "G")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:108 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "G")) ")" ) ($#k14_member_1 :::"///"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set "(" (Set (Var "G")) ($#k14_member_1 :::"///"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:109 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G")) ")" ) ($#k12_member_1 :::"**"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k12_member_1 :::"**"::: ) (Set (Var "H")) ")" ) ($#k14_member_1 :::"///"::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:110 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set (Var "G")) ")" ) ($#k14_member_1 :::"///"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set "(" (Set (Var "G")) ($#k12_member_1 :::"**"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEMBER_1:111 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k14_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "g")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "g")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:112 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k14_member_1 :::"///"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:113 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k14_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "h")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:114 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) ) ($#k14_member_1 :::"///"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "h")) "," (Set (Var "i")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "i")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; func "A" :::"///"::: "B" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 12 (Set "A" ($#k13_member_1 :::"**"::: ) (Set "(" "B" ($#k7_member_1 :::""""::: ) ")" )); end; :: deftheorem defines :::"///"::: MEMBER_1:def 12 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k7_member_1 :::""""::: ) ")" )))); theorem :: MEMBER_1:115 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c1")) ($#k6_binop_2 :::"/"::: ) (Set (Var "c2")) ")" ) where c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) ; theorem :: MEMBER_1:116 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k15_member_1 :::"///"::: ) "B") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "B" ($#k15_member_1 :::"///"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k15_member_1 :::"///"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A", "B" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k15_member_1 :::"///"::: ) "B") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k15_member_1 :::"///"::: ) "B") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A", "B" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k15_member_1 :::"///"::: ) "B") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A", "B" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; theorem :: MEMBER_1:117 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k15_member_1 :::"///"::: ) (Set (Var "D"))))) ; theorem :: MEMBER_1:118 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:119 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:120 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:121 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k5_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")) ")" )))) ; theorem :: MEMBER_1:122 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "B")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:123 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" ) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "B")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:124 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:125 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")) ")" ) ($#k13_member_1 :::"**"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:126 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set (Var "B")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set "(" (Set (Var "B")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" )))) ; theorem :: MEMBER_1:127 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set "(" (Set (Var "B")) ($#k15_member_1 :::"///"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "C")) ")" ) ($#k15_member_1 :::"///"::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:128 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k15_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "b")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:129 (Bool "for" (Set (Var "a")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k15_member_1 :::"///"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "t")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:130 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "s")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k15_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "b")) ($#k6_binop_2 :::"/"::: ) (Set (Var "s")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:131 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k15_member_1 :::"///"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "t")) ")" ) "," (Set "(" (Set (Var "b")) ($#k6_binop_2 :::"/"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "b")) ($#k6_binop_2 :::"/"::: ) (Set (Var "t")) ")" ) ($#k2_enumset1 :::"}"::: ) ))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"++"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 13 (Set (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) ($#k8_member_1 :::"++"::: ) "F"); end; :: deftheorem defines :::"++"::: MEMBER_1:def 13 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k8_member_1 :::"++"::: ) (Set (Var "F")))))); theorem :: MEMBER_1:132 (Bool "for" (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set (Var "G")))))) ; theorem :: MEMBER_1:133 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: MEMBER_1:134 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_xxreal_3 :::"+"::: ) (Set (Var "w")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k16_member_1 :::"++"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k16_member_1 :::"++"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k16_member_1 :::"++"::: ) "F") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:135 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:136 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:137 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:138 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k16_member_1 :::"++"::: ) (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:139 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:140 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set "(" (Set (Var "F")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "F")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "r")) ($#k16_member_1 :::"++"::: ) (Set (Var "G")) ")" ))))) ; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"++"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 14 (Set (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k9_member_1 :::"++"::: ) "A"); end; :: deftheorem defines :::"++"::: MEMBER_1:def 14 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k9_member_1 :::"++"::: ) (Set (Var "A")))))); theorem :: MEMBER_1:141 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A")))))) ; theorem :: MEMBER_1:142 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ; theorem :: MEMBER_1:143 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "a" ($#k17_member_1 :::"++"::: ) "A") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: MEMBER_1:144 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MEMBER_1:145 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:146 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: MEMBER_1:147 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k17_member_1 :::"++"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set "(" (Set (Var "b")) ($#k17_member_1 :::"++"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEMBER_1:148 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A")) ")" ) ($#k9_member_1 :::"++"::: ) (Set (Var "B")))))) ; theorem :: MEMBER_1:149 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:150 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:151 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "A")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "a")) ($#k17_member_1 :::"++"::: ) (Set (Var "B")) ")" ))))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"--"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 15 (Set (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) ($#k10_member_1 :::"--"::: ) "F"); end; :: deftheorem defines :::"--"::: MEMBER_1:def 15 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k18_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k10_member_1 :::"--"::: ) (Set (Var "F")))))); theorem :: MEMBER_1:152 (Bool "for" (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k18_member_1 :::"--"::: ) (Set (Var "G")))))) ; theorem :: MEMBER_1:153 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k18_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: MEMBER_1:154 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k18_member_1 :::"--"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "w")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k18_member_1 :::"--"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k18_member_1 :::"--"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k18_member_1 :::"--"::: ) "F") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:155 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:156 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; theorem :: MEMBER_1:157 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:158 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:159 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "F")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "r")) ($#k18_member_1 :::"--"::: ) (Set (Var "G")) ")" ))))) ; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"--"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 16 (Set (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k11_member_1 :::"--"::: ) "A"); end; :: deftheorem defines :::"--"::: MEMBER_1:def 16 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k11_member_1 :::"--"::: ) (Set (Var "A")))))); theorem :: MEMBER_1:160 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A")))))) ; theorem :: MEMBER_1:161 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ; theorem :: MEMBER_1:162 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k19_member_1 :::"--"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k19_member_1 :::"--"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k19_member_1 :::"--"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k19_member_1 :::"--"::: ) "A") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k19_member_1 :::"--"::: ) "A") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k19_member_1 :::"--"::: ) "A") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: MEMBER_1:163 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MEMBER_1:164 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:165 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:166 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:167 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "B")) ")" ))))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func "F" :::"--"::: "f" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 17 (Set "F" ($#k10_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"--"::: MEMBER_1:def 17 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k10_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))))); theorem :: MEMBER_1:168 (Bool "for" (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k20_member_1 :::"--"::: ) (Set (Var "f")))))) ; theorem :: MEMBER_1:169 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "f")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: MEMBER_1:170 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_xxreal_3 :::"-"::: ) (Set (Var "f")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "F" ($#k20_member_1 :::"--"::: ) "f") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "F" ($#k20_member_1 :::"--"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "F" ($#k20_member_1 :::"--"::: ) "f") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:171 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "f")) ($#k18_member_1 :::"--"::: ) (Set (Var "F")) ")" ))))) ; theorem :: MEMBER_1:172 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k18_member_1 :::"--"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_member_1 :::"--"::: ) (Set "(" (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "f")) ")" ))))) ; theorem :: MEMBER_1:173 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" ) ($#k20_member_1 :::"--"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "r")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "G")) ($#k20_member_1 :::"--"::: ) (Set (Var "r")) ")" ))))) ; theorem :: MEMBER_1:174 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" ) ($#k20_member_1 :::"--"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "r")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k20_member_1 :::"--"::: ) (Set (Var "r")) ")" ))))) ; theorem :: MEMBER_1:175 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "G")) ")" ) ($#k20_member_1 :::"--"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k20_member_1 :::"--"::: ) (Set (Var "r")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "G")) ($#k20_member_1 :::"--"::: ) (Set (Var "r")) ")" ))))) ; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "A" :::"--"::: "a" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 18 (Set "A" ($#k11_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"--"::: MEMBER_1:def 18 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))))); theorem :: MEMBER_1:176 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b")) ($#k4_binop_2 :::"-"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")))))) ; theorem :: MEMBER_1:177 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c")) ($#k4_binop_2 :::"-"::: ) (Set (Var "a")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ; theorem :: MEMBER_1:178 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k4_binop_2 :::"-"::: ) (Set (Var "a")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k21_member_1 :::"--"::: ) "a") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k21_member_1 :::"--"::: ) "a") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k21_member_1 :::"--"::: ) "a") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k21_member_1 :::"--"::: ) "a") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k21_member_1 :::"--"::: ) "a") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k21_member_1 :::"--"::: ) "a") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: MEMBER_1:179 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")))) ")" ))) ; theorem :: MEMBER_1:180 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:181 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEMBER_1:182 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k19_member_1 :::"--"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:183 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:184 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" ) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "B")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:185 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" ) ($#k21_member_1 :::"--"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "B")) ($#k21_member_1 :::"--"::: ) (Set (Var "a")) ")" ))))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"**"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 19 (Set (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) ($#k12_member_1 :::"**"::: ) "F"); end; :: deftheorem defines :::"**"::: MEMBER_1:def 19 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k12_member_1 :::"**"::: ) (Set (Var "F")))))); theorem :: MEMBER_1:186 (Bool "for" (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set (Var "G")))))) ; theorem :: MEMBER_1:187 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: MEMBER_1:188 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "w")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k22_member_1 :::"**"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k22_member_1 :::"**"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k22_member_1 :::"**"::: ) "F") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; theorem :: MEMBER_1:189 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set "(" (Set (Var "F")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:190 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k22_member_1 :::"**"::: ) (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:191 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set "(" (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEMBER_1:192 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set "(" (Set (Var "F")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set (Var "F")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "r")) ($#k22_member_1 :::"**"::: ) (Set (Var "G")) ")" ))))) ; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"**"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 20 (Set (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k13_member_1 :::"**"::: ) "A"); end; :: deftheorem defines :::"**"::: MEMBER_1:def 20 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k13_member_1 :::"**"::: ) (Set (Var "A")))))); theorem :: MEMBER_1:193 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")))))) ; theorem :: MEMBER_1:194 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ; theorem :: MEMBER_1:195 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "A" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "a" ($#k23_member_1 :::"**"::: ) "A") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: MEMBER_1:196 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:197 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:198 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:199 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:200 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:201 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:202 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MEMBER_1:203 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 1) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: MEMBER_1:204 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "b")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEMBER_1:205 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "A")) ($#k13_member_1 :::"**"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ) ($#k13_member_1 :::"**"::: ) (Set (Var "B")))))) ; theorem :: MEMBER_1:206 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "b")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEMBER_1:207 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k23_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "b")) ($#k23_member_1 :::"**"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEMBER_1:208 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k9_member_1 :::"++"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "C")) ")" ))))) ; theorem :: MEMBER_1:209 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set "(" (Set (Var "B")) ($#k11_member_1 :::"--"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "B")) ")" ) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "a")) ($#k23_member_1 :::"**"::: ) (Set (Var "C")) ")" ))))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"///"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 21 (Set (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) ($#k14_member_1 :::"///"::: ) "F"); end; :: deftheorem defines :::"///"::: MEMBER_1:def 21 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k24_member_1 :::"///"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k14_member_1 :::"///"::: ) (Set (Var "F")))))); theorem :: MEMBER_1:210 (Bool "for" (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k24_member_1 :::"///"::: ) (Set (Var "G")))))) ; theorem :: MEMBER_1:211 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k24_member_1 :::"///"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: MEMBER_1:212 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k24_member_1 :::"///"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "w")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k24_member_1 :::"///"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k24_member_1 :::"///"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k24_member_1 :::"///"::: ) "F") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"///"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 22 (Set (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k15_member_1 :::"///"::: ) "A"); end; :: deftheorem defines :::"///"::: MEMBER_1:def 22 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k15_member_1 :::"///"::: ) (Set (Var "A")))))); theorem :: MEMBER_1:213 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")))))) ; theorem :: MEMBER_1:214 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ; theorem :: MEMBER_1:215 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_binop_2 :::"/"::: ) (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k25_member_1 :::"///"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k25_member_1 :::"///"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k25_member_1 :::"///"::: ) "A") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k25_member_1 :::"///"::: ) "A") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k25_member_1 :::"///"::: ) "A") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: MEMBER_1:216 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:217 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:218 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:219 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:220 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MEMBER_1:221 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "b")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEMBER_1:222 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k25_member_1 :::"///"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "b")) ($#k25_member_1 :::"///"::: ) (Set (Var "A")) ")" ))))) ; definitionlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func "F" :::"///"::: "f" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 23 (Set "F" ($#k14_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"///"::: MEMBER_1:def 23 : (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k26_member_1 :::"///"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k14_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))))); theorem :: MEMBER_1:223 (Bool "for" (Set (Var "G")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "g")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k26_member_1 :::"///"::: ) (Set (Var "f")))))) ; theorem :: MEMBER_1:224 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k26_member_1 :::"///"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "f")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: MEMBER_1:225 (Bool "for" (Set (Var "F")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k26_member_1 :::"///"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k6_xxreal_3 :::"/"::: ) (Set (Var "f")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "F" ($#k26_member_1 :::"///"::: ) "f") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "F" ($#k26_member_1 :::"///"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "F" ($#k26_member_1 :::"///"::: ) "f") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; definitionlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "A" :::"///"::: "a" -> ($#m1_hidden :::"set"::: ) equals :: MEMBER_1:def 24 (Set "A" ($#k15_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"///"::: MEMBER_1:def 24 : (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k15_member_1 :::"///"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))))); theorem :: MEMBER_1:226 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b")) ($#k6_binop_2 :::"/"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")))))) ; theorem :: MEMBER_1:227 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "c")) ($#k6_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) where c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ; theorem :: MEMBER_1:228 (Bool "for" (Set (Var "A")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k6_binop_2 :::"/"::: ) (Set (Var "a")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k27_member_1 :::"///"::: ) "a") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k27_member_1 :::"///"::: ) "a") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k27_member_1 :::"///"::: ) "a") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k27_member_1 :::"///"::: ) "a") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "A" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "A" ($#k27_member_1 :::"///"::: ) "a") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: MEMBER_1:229 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:230 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MEMBER_1:231 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:232 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B")) ")" ) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:233 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "B")) ")" ) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:234 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_member_1 :::"++"::: ) (Set (Var "B")) ")" ) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ))))) ; theorem :: MEMBER_1:235 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_member_1 :::"--"::: ) (Set (Var "B")) ")" ) ($#k27_member_1 :::"///"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ) ($#k11_member_1 :::"--"::: ) (Set "(" (Set (Var "B")) ($#k27_member_1 :::"///"::: ) (Set (Var "a")) ")" ))))) ;