:: EQREL_1 semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"nabla"::: "X" -> ($#m1_subset_1 :::"Relation":::) "of" "X" equals :: EQREL_1:def 1 (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ); end; :: deftheorem defines :::"nabla"::: EQREL_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_eqrel_1 :::"nabla"::: ) "X") -> ($#v1_relat_2 :::"reflexive"::: ) ($#v1_partfun1 :::"total"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R1", "R2" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); :: original: :::"/\"::: redefine func "R1" :::"/\"::: "R2" -> ($#m1_subset_1 :::"Relation":::) "of" "X"; :: original: :::"\/"::: redefine func "R1" :::"\/"::: "R2" -> ($#m1_subset_1 :::"Relation":::) "of" "X"; end; theorem :: EQREL_1:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")) ")" ) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "R1"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")))))) ; theorem :: EQREL_1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "X"))) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))) ")" )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Tolerance of "X" is ($#v1_relat_2 :::"reflexive"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" "X"; mode Equivalence_Relation of "X" is ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" "X"; end; theorem :: EQREL_1:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")))) ; theorem :: EQREL_1:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_eqrel_1 :::"nabla"::: ) "X") -> ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v1_partfun1 :::"total"::: ) ; end; theorem :: EQREL_1:5 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_relat_2 :::"reflexive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ; theorem :: EQREL_1:6 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v3_relat_2 :::"symmetric"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ; theorem :: EQREL_1:7 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v8_relat_2 :::"transitive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ; theorem :: EQREL_1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_relat_2 :::"reflexive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: EQREL_1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_relat_2 :::"symmetric"::: ) ) & (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) ) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "EqR1", "EqR2" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); :: original: :::"/\"::: redefine func "EqR1" :::"/\"::: "EqR2" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X"; end; theorem :: EQREL_1:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k4_eqrel_1 :::"/\"::: ) (Set (Var "EqR"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: EQREL_1:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SFXX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "SFXX")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFXX")))) "holds" (Bool (Set (Var "Y")) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X"))) ")" )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "SFXX"))) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X"))))) ; theorem :: EQREL_1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR"))) & (Bool "(" "for" (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR2")))) "holds" (Bool (Set (Var "EqR")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR2"))) ")" ) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "EqR1", "EqR2" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); func "EqR1" :::""\/""::: "EqR2" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" means :: EQREL_1:def 2 (Bool "(" (Bool (Set "EqR1" ($#k3_eqrel_1 :::"\/"::: ) "EqR2") ($#r1_relset_1 :::"c="::: ) it) & (Bool "(" "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" "st" (Bool (Bool (Set "EqR1" ($#k3_eqrel_1 :::"\/"::: ) "EqR2") ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR")))) "holds" (Bool it ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR"))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "b1"))) & (Bool "(" "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR")))) "holds" (Bool (Set (Var "b1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR"))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "EqR2")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR1"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "b1"))) & (Bool "(" "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "EqR2")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR1"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR")))) "holds" (Bool (Set (Var "b1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR"))) ")" ) ")" )) ; idempotence (Bool "for" (Set (Var "EqR1")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")) "holds" (Bool "(" (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR1"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR1"))) & (Bool "(" "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR1"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR")))) "holds" (Bool (Set (Var "EqR1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR"))) ")" ) ")" )) ; end; :: deftheorem defines :::""\/""::: EQREL_1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR2")))) "iff" (Bool "(" (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "b4"))) & (Bool "(" "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR")))) "holds" (Bool (Set (Var "b4")) ($#r1_relset_1 :::"c="::: ) (Set (Var "EqR"))) ")" ) ")" ) ")" ))); theorem :: EQREL_1:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "EqR3")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR2")) ")" ) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR3"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set "(" (Set (Var "EqR2")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR3")) ")" ))))) ; theorem :: EQREL_1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "EqR")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR"))) ($#r2_relset_1 :::"="::: ) (Set (Var "EqR"))))) ; theorem :: EQREL_1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR2"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "EqR2")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR1")))))) ; theorem :: EQREL_1:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "EqR1")) ($#k4_eqrel_1 :::"/\"::: ) (Set "(" (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "EqR1"))))) ; theorem :: EQREL_1:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set "(" (Set (Var "EqR1")) ($#k4_eqrel_1 :::"/\"::: ) (Set (Var "EqR2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "EqR1"))))) ; scheme :: EQREL_1:sch 1 ExEqRel{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "EqR"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "x"))])) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) proof end; notationlet "R" be ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; synonym :::"Class"::: "(" "R" "," "x" ")" for :::"Im"::: "(" "R" "," "x" ")" ; end; 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: :::"Class"::: redefine func :::"Class"::: "(" "R" "," "x" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "Y"; end; theorem :: EQREL_1:18 (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 :::"Class"::: ) "(" (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 :: EQREL_1:19 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v3_relat_2 :::"symmetric"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" )) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ))) ; theorem :: EQREL_1:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ))))) ; theorem :: EQREL_1:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "y")) ")" )))))) ; theorem :: EQREL_1:22 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v8_relat_2 :::"transitive"::: ) ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ; theorem :: EQREL_1:23 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" )) "iff" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" )) ")" )))) ; theorem :: EQREL_1:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" )) "or" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" )) ")" )))) ; theorem :: EQREL_1:25 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: EQREL_1:26 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: EQREL_1:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "EqR")) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")))))) ; theorem :: EQREL_1:28 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "EqR1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "EqR2")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2")))) ")" ) ")" )) ")" ))) ; theorem :: EQREL_1:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "E")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR1")) "," (Set (Var "x")) ")" )) "or" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR2")) "," (Set (Var "x")) ")" )) ")" )))) ; theorem :: EQREL_1:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "EqR1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "EqR2"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")))) "or" (Bool (Set (Var "EqR1")) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")))) "or" (Bool (Set (Var "EqR2")) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "X")))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "EqR" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); func :::"Class"::: "EqR" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: EQREL_1:def 3 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "EqR" "," (Set (Var "x")) ")" )) ")" )) ")" )); end; :: deftheorem defines :::"Class"::: EQREL_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_eqrel_1 :::"Class"::: ) (Set (Var "EqR")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" )) ")" )) ")" )) ")" )))); theorem :: EQREL_1:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k7_eqrel_1 :::"Class"::: ) (Set (Var "EqR"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"a_partition"::: "of" "X" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: EQREL_1:def 4 (Bool "(" (Bool (Set ($#k5_setfam_1 :::"union"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool "(" "not" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) it) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) ")" ) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"a_partition"::: EQREL_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))); theorem :: EQREL_1:32 (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: EQREL_1:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_eqrel_1 :::"Class"::: ) (Set (Var "EqR"))) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))))) ; theorem :: EQREL_1:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k7_eqrel_1 :::"Class"::: ) (Set (Var "EqR"))))))) ; theorem :: EQREL_1:35 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "EqR"))) "iff" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" )) ")" )))) ; theorem :: EQREL_1:36 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_eqrel_1 :::"Class"::: ) (Set (Var "EqR"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" ))))) ; begin registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); :: original: :::"Class"::: redefine func :::"Class"::: "R" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "I")); cluster (Set ($#k7_eqrel_1 :::"Class"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "I")); cluster (Set ($#k7_eqrel_1 :::"Class"::: ) "R") -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; notationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "I")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); synonym :::"EqClass"::: "(" "R" "," "x" ")" for :::"Class"::: "(" "I" "," "R" ")" ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "I")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"Class"::: redefine func :::"EqClass"::: "(" "R" "," "x" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "R"); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"SmallestPartition"::: "X" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X" equals :: EQREL_1:def 5 (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) "X" ")" )); end; :: deftheorem defines :::"SmallestPartition"::: EQREL_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" )))); theorem :: EQREL_1:37 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool verum) "}" )) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "S1" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); func :::"EqClass"::: "(" "x" "," "S1" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: EQREL_1:def 6 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) it) & (Bool it ($#r2_hidden :::"in"::: ) "S1") ")" ); end; :: deftheorem defines :::"EqClass"::: EQREL_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "S1")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S1")) ")" )) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "S1"))) ")" ) ")" ))))); theorem :: EQREL_1:38 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S2")) ")" )) ")" )) "holds" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Var "S2"))))) ; theorem :: EQREL_1:39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Family-Class of "X" is ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Family-Class":::) "of" (Set (Const "X")); attr "F" is :::"partition-membered"::: means :: EQREL_1:def 7 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "S")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X")); end; :: deftheorem defines :::"partition-membered"::: EQREL_1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Family-Class":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_eqrel_1 :::"partition-membered"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "S")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")))) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_eqrel_1 :::"partition-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ")" )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Part-Family of "X" is ($#v1_eqrel_1 :::"partition-membered"::: ) ($#m1_subset_1 :::"Family-Class":::) "of" "X"; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; theorem :: EQREL_1:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Part-Family":::) "of" (Set (Var "X"))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_eqrel_1 :::"partition-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ")" )); end; theorem :: EQREL_1:41 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S1")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "S1")) ")" ))) "holds" (Bool (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "S1")) ")" ))))) ; theorem :: EQREL_1:42 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S")) ")" )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Part-Family":::) "of" (Set (Const "X")); func :::"Intersection"::: "F" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X" means :: EQREL_1:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," it ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S")) ")" ")" ) where S "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X" : (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) "F") "}" ))); end; :: deftheorem defines :::"Intersection"::: EQREL_1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Part-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_eqrel_1 :::"Intersection"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "b3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k11_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "x")) "," (Set (Var "S")) ")" ")" ) where S "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ")" )))); theorem :: EQREL_1:43 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "S")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "S")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" )))))) ; theorem :: EQREL_1:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "S")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))))))) ; theorem :: EQREL_1:45 (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set ($#k1_xboole_0 :::"{}"::: ) )) ; begin theorem :: EQREL_1:46 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_relat_1 :::"""::: ) (Set (Var "X1"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "X1"))))) ; theorem :: EQREL_1:47 (Bool "for" (Set (Var "e")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "e"))))) ; theorem :: EQREL_1:48 (Bool "for" (Set (Var "e")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "e"))))) ; theorem :: EQREL_1:49 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X1"))) & (Bool (Set (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "Y1"))) ")" )))) ; theorem :: EQREL_1:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X1"))) & (Bool (Set (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "Y1"))) ")" )))) ; theorem :: EQREL_1:51 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool "ex" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))(Bool "ex" (Set (Var "Y1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) )))) ")" ) ")" )) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: EQREL_1:52 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool "ex" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))(Bool "ex" (Set (Var "Y1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) )))) ")" ) ")" )) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" (Set "(" ($#k1_funct_3 :::".:"::: ) (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: EQREL_1:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set "(" ($#k2_funct_3 :::".:"::: ) (Set (Var "f")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "H")) ")" ))))))) ; theorem :: EQREL_1:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) "}" )))) ; theorem :: EQREL_1:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))))))) ; theorem :: EQREL_1:56 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "x9"))))) "holds" (Bool (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "x9")))) ")" )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Set (Set (Var "H")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Var "G"))))))) ; theorem :: EQREL_1:57 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: EQREL_1:58 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Z")) "holds" (Bool (Set (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "F")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k16_funct_3 :::":]"::: ) ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: EQREL_1:59 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Z")) "holds" (Bool (Set (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "F")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k16_funct_3 :::":]"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_mcart_1 :::":]"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" (Set (Var "F")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) "," (Set (Var "B")) ($#k8_mcart_1 :::":]"::: ) )))))) ; theorem :: EQREL_1:60 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Z")) "holds" (Bool (Set (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "F")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k16_funct_3 :::":]"::: ) ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) )))))) ; theorem :: EQREL_1:61 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")))))) ; theorem :: EQREL_1:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "B")) ")" )))))) ; theorem :: EQREL_1:63 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))))))) ; theorem :: EQREL_1:64 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool (Bool "not" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); func :::"proj"::: "D" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," "D" means :: EQREL_1:def 9 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "p"))))); end; :: deftheorem defines :::"proj"::: EQREL_1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))))) ")" )))); theorem :: EQREL_1:65 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))))))) ; theorem :: EQREL_1:66 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: EQREL_1:67 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))))))) ; theorem :: EQREL_1:68 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "W")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "ex" (Set (Var "W9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Set "(" ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "W9"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))))) ; theorem :: EQREL_1:69 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "W")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "W"))) ")" )) "holds" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")) ")" ) ($#k8_relset_1 :::"""::: ) (Set "(" (Set "(" ($#k13_eqrel_1 :::"proj"::: ) (Set (Var "D")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "W")) ")" )))))) ; theorem :: EQREL_1:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ;