:: RELSET_2 semantic presentation begin notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"{_{":::"X":::"}_}"::: for :::"SmallestPartition"::: "X"; end; theorem :: RELSET_2:1 (Bool "for" (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) ; theorem :: RELSET_2:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: RELSET_2:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "Y")) ($#k10_eqrel_1 :::"}_}"::: ) )))) ; theorem :: RELSET_2:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "Y")) ($#k10_eqrel_1 :::"}_}"::: ) )))) ; theorem :: RELSET_2:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "Y")) ($#k10_eqrel_1 :::"}_}"::: ) )))) ; theorem :: RELSET_2:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "Y")) ($#k10_eqrel_1 :::"}_}"::: ) )) ")" )) ; theorem :: RELSET_2:7 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "B1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "B2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" (Set (Var "B1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B2")) ")" ))))) ; theorem :: RELSET_2:8 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Q")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "Q")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )))) ; begin theorem :: RELSET_2:9 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" )) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ))) ; theorem :: RELSET_2:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "(" (Set (Var "R1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "R2")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R1")) "," (Set (Var "x")) ")" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R2")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: RELSET_2:11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "(" (Set (Var "R1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "R2")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R1")) "," (Set (Var "x")) ")" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R2")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: RELSET_2:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "(" (Set (Var "R1")) ($#k6_subset_1 :::"\"::: ) (Set (Var "R2")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R1")) "," (Set (Var "x")) ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R2")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: RELSET_2:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "R2")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R1")) ($#k7_relat_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "R2")) ($#k7_relat_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ")" ))))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"Im"::: redefine func :::"Im"::: "(" "R" "," "x" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "Y"; :: original: :::"Coim"::: redefine func :::"Coim"::: "(" "R" "," "x" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: RELSET_2:14 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: RELSET_2:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )))) ; theorem :: RELSET_2:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "{" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A"))))) ; theorem :: RELSET_2:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )))))) ; theorem :: RELSET_2:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "{" (Set "(" (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B"))))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); func :::".:"::: "(" "R" "," "A" ")" -> ($#m1_hidden :::"Function":::) means :: RELSET_2:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "A")) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) "A")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set "R" ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))) ")" ) ")" ); end; :: deftheorem defines :::".:"::: RELSET_2:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_relset_2 :::".:"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))) ")" ) ")" ) ")" )))); notationlet "B", "A" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ); synonym :::".:"::: "R" for :::".:"::: "(" "A" "," "B" ")" ; end; theorem :: RELSET_2:19 (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_relset_2 :::".:"::: ) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_relset_2 :::".:"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")))))) ; theorem :: RELSET_2:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k3_relset_2 :::".:"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")) ")" ))))) ; theorem :: RELSET_2:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k3_relset_2 :::".:"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")) ")" ) ")" )))) ; definitionlet "B", "A" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::".:"::: redefine func :::".:"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "A" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "B" ")" ); end; theorem :: RELSET_2:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set "(" ($#k4_relset_2 :::".:"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" ))))) ; begin definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ); func "R" :::".:^"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: RELSET_2:def 2 (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" (Set "(" ($#k4_relset_2 :::".:"::: ) "R" ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) "X" ($#k10_eqrel_1 :::"}_}"::: ) ) ")" )); end; :: deftheorem defines :::".:^"::: RELSET_2:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "R")) ($#k5_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" (Set "(" ($#k4_relset_2 :::".:"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) ")" )))))); definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::".:^"::: redefine func "R" :::".:^"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "B"; end; theorem :: RELSET_2:23 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_relset_2 :::".:"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: RELSET_2:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" )))))) ; theorem :: RELSET_2:25 (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ))) ")" )))))) ; theorem :: RELSET_2:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k4_relset_2 :::".:"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X1")) ($#k10_eqrel_1 :::"}_}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "X1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X2"))))))) ; theorem :: RELSET_2:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "X1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X2")) ")" )))))) ; theorem :: RELSET_2:28 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "{" (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B"))))))) ; theorem :: RELSET_2:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "B")))))) ; theorem :: RELSET_2:30 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "Y")) ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) : (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "G"))))))))) ; theorem :: RELSET_2:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X1"))))))) ; theorem :: RELSET_2:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "X1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "X2")) ")" )))))) ; theorem :: RELSET_2:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "R2")) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "R2")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" )))))) ; theorem :: RELSET_2:34 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "FR")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "FR")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" ) where R "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "R")) ($#r2_hidden :::"in"::: ) (Set (Var "FR"))) "}" ))))) ; theorem :: RELSET_2:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "FR")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "{" (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) where R "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "R")) ($#r2_hidden :::"in"::: ) (Set (Var "FR"))) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B"))))))) ; theorem :: RELSET_2:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: RELSET_2:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "B")))))) ; theorem :: RELSET_2:38 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "FR")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) where R "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "R")) ($#r2_hidden :::"in"::: ) (Set (Var "FR"))) "}" )) "holds" (Bool (Set (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "FR")) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "G")))))))) ; theorem :: RELSET_2:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "R2")))) "holds" (Bool (Set (Set (Var "R1")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R2")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))))))) ; theorem :: RELSET_2:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "R2")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "R2")) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))))))) ; theorem :: RELSET_2:41 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_2 :::"Im"::: ) "(" (Set "(" (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) ")" ))) ; theorem :: RELSET_2:42 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))))) ; theorem :: RELSET_2:43 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y")))) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_2 :::"Im"::: ) "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) "," (Set (Var "y")) ")" )) ")" )) ")" )))) ; theorem :: RELSET_2:44 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_2 :::"Im"::: ) "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) "," (Set (Var "y")) ")" )) ")" )) "iff" (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")))) ")" )))) ; theorem :: RELSET_2:45 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")))) ")" ))))) ; theorem :: RELSET_2:46 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "R")) ")" ) ")" )))))) ; theorem :: RELSET_2:47 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "Y")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "R")) ")" ) ")" )))))) ; theorem :: RELSET_2:48 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))))) ; definitionlet "A", "B", "C" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "B")) "," (Set (Const "C")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"*"::: redefine func "R" :::"*"::: "S" -> ($#m1_subset_1 :::"Relation":::) "of" "A" "," "C"; end; theorem :: RELSET_2:49 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))))))) ; theorem :: RELSET_2:50 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))) ")" ))) ; theorem :: RELSET_2:51 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "S")) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set (Var "S")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "R")))) ")" )))) ; theorem :: RELSET_2:52 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "R")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set (Var "S")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "S")))) ")" )))) ; theorem :: RELSET_2:53 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")))) ")" )))) ; theorem :: RELSET_2:54 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_2 :::"*"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y")))) ")" )))) ; theorem :: RELSET_2:55 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "R")) ")" ))) ")" ))) ; theorem :: RELSET_2:56 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))))) ; theorem :: RELSET_2:57 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_2 :::"*"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")))))) ; theorem :: RELSET_2:58 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "S")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "R")) ($#k7_relset_2 :::"*"::: ) (Set "(" (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")))))))) ; theorem :: RELSET_2:59 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k3_relset_1 :::"~"::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: RELSET_2:60 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")))) ")" ))))) ; theorem :: RELSET_2:61 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k3_subset_1 :::"`"::: ) )) "iff" (Bool (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))))) ; theorem :: RELSET_2:62 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "Y")) ")" ))) ")" ))))) ; theorem :: RELSET_2:63 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set (Var "X")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set (Var "R")) ($#k6_relset_2 :::".:^"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" ) ($#k6_relset_2 :::".:^"::: ) (Set (Var "Y")) ")" ) ")" ))) ")" ))))) ; theorem :: RELSET_2:64 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "B")) ")" ))))) ;