:: RELAT_1 semantic presentation begin definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"Relation-like"::: means :: RELAT_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"Relation-like"::: RELAT_1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_relat_1 :::"Relation-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )))) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_relat_1 :::"Relation-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode Relation is ($#v1_relat_1 :::"Relation-like"::: ) ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; scheme :: RELAT_1:sch 1 RelExistence{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "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 "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ))) proof end; definitionlet "P", "R" be ($#m1_hidden :::"Relation":::); redefine pred "P" :::"="::: "R" means :: RELAT_1:def 2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "P") "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" )); end; :: deftheorem defines :::"="::: RELAT_1:def 2 : (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ")" )); registrationlet "P" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "P" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v1_relat_1 :::"Relation-like"::: ) ; cluster (Set "P" ($#k4_xboole_0 :::"\"::: ) "X") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "P", "R" be ($#m1_hidden :::"Relation":::); cluster (Set "P" ($#k2_xboole_0 :::"\/"::: ) "R") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "R", "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "a", "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "b" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "a" "," "b" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "b" ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) "c" "," "d" ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; definitionlet "P" be ($#m1_hidden :::"Relation":::); let "A" be ($#m1_hidden :::"set"::: ) ; redefine pred "P" :::"c="::: "A" means :: RELAT_1:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "A")); end; :: deftheorem defines :::"c="::: RELAT_1:def 3 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))); notationlet "R" be ($#m1_hidden :::"Relation":::); synonym :::"dom"::: "R" for :::"proj1"::: "R"; end; theorem :: RELAT_1:1 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )))) ; theorem :: RELAT_1:2 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )))) ; theorem :: RELAT_1:3 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k6_subset_1 :::"\"::: ) (Set (Var "R")) ")" )))) ; notationlet "R" be ($#m1_hidden :::"Relation":::); synonym :::"rng"::: "R" for :::"proj2"::: "R"; end; theorem :: RELAT_1:4 canceled; theorem :: RELAT_1:5 canceled; theorem :: RELAT_1:6 canceled; theorem :: RELAT_1:7 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: RELAT_1:8 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "R")))) ; theorem :: RELAT_1:9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: RELAT_1:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "x")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" ))) ; theorem :: RELAT_1:11 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) ")" )) ; theorem :: RELAT_1:12 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "P")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" )))) ; theorem :: RELAT_1:13 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "P")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" )))) ; theorem :: RELAT_1:14 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "P")) ($#k6_subset_1 :::"\"::: ) (Set (Var "R")) ")" )))) ; definitioncanceled; canceled; let "R" be ($#m1_hidden :::"Relation":::); func :::"field"::: "R" -> ($#m1_hidden :::"set"::: ) equals :: RELAT_1:def 6 (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "R" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "R" ")" )); end; :: deftheorem RELAT_1:def 4 : canceled; :: deftheorem RELAT_1:def 5 : canceled; :: deftheorem defines :::"field"::: RELAT_1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" )))); theorem :: RELAT_1:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) ")" ))) ; theorem :: RELAT_1:16 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: RELAT_1:18 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" (Set (Var "P")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "P")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" )))) ; theorem :: RELAT_1:19 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" (Set (Var "P")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "P")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" )))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); func "R" :::"~"::: -> ($#m1_hidden :::"Relation":::) means :: RELAT_1:def 7 (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"::: ) it) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" )); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (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 "b1"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" )) "holds" (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 "b2"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ))) ; end; :: deftheorem defines :::"~"::: RELAT_1:def 7 : (Bool "for" (Set (Var "R")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) "iff" (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 "b2"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ")" )); theorem :: RELAT_1:20 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ))) ")" )) ; theorem :: RELAT_1:21 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )))) ; theorem :: RELAT_1:22 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "R")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )))) ; theorem :: RELAT_1:23 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "R")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )))) ; theorem :: RELAT_1:24 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k6_subset_1 :::"\"::: ) (Set (Var "R")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )))) ; definitionlet "P", "R" be ($#m1_hidden :::"set"::: ) ; func "P" :::"(#)"::: "R" -> ($#m1_hidden :::"Relation":::) means :: RELAT_1:def 8 (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"::: ) it) "iff" (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" )) ")" )); end; :: deftheorem defines :::"(#)"::: RELAT_1:def 8 : (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_relat_1 :::"(#)"::: ) (Set (Var "R")))) "iff" (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 "b3"))) "iff" (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ")" )) ")" ))); notationlet "P", "R" be ($#m1_hidden :::"Relation":::); synonym "P" :::"*"::: "R" for "P" :::"(#)"::: "R"; end; theorem :: RELAT_1:25 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))))) ; theorem :: RELAT_1:26 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:27 (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:28 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P"))))) ; theorem :: RELAT_1:29 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "Q")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Q")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:30 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Q")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:31 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))))) ; theorem :: RELAT_1:32 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q")) ")" )))) ; theorem :: RELAT_1:33 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Q")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q")) ")" )))) ; theorem :: RELAT_1:34 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Q")) ")" )))) ; theorem :: RELAT_1:35 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k2_relat_1 :::"~"::: ) ")" )))) ; theorem :: RELAT_1:36 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q")) ")" )))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: RELAT_1:37 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" )) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: RELAT_1:38 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: RELAT_1:39 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); cluster (Set "X" ($#k3_relat_1 :::"(#)"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set "R" ($#k3_relat_1 :::"(#)"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:40 (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: RELAT_1:41 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: RELAT_1:42 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_relat_1 :::"~"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:43 (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: RELAT_1:44 (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"non-empty"::: means :: RELAT_1:def 9 (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))); end; :: deftheorem defines :::"non-empty"::: RELAT_1:def 9 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) "iff" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"(#)"::: ) "S") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"id"::: "X" -> ($#m1_hidden :::"Relation":::) means :: RELAT_1:def 10 (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"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" )); end; :: deftheorem defines :::"id"::: RELAT_1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))) "iff" (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 "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" )) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; reduce ; reduce ; end; theorem :: RELAT_1:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; reduce ; end; theorem :: RELAT_1:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))))) ; theorem :: RELAT_1:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "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"))) ")" )) "holds" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:48 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ))) ; theorem :: RELAT_1:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ))) ; theorem :: RELAT_1:50 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" ))) ; theorem :: RELAT_1:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:52 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R")))) ; theorem :: RELAT_1:53 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:54 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R")))) ; theorem :: RELAT_1:55 (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: RELAT_1:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P2")) "," (Set (Var "R")) "," (Set (Var "P1")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P2"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "P2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P1")) ")" ))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P2"))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; func "R" :::"|"::: "X" -> ($#m1_hidden :::"Relation":::) means :: RELAT_1:def 11 (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"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" )); end; :: deftheorem defines :::"|"::: RELAT_1:def 11 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))) "iff" (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 "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" )) ")" )))); registrationlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:57 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) ")" ) ")" ))) ; theorem :: RELAT_1:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))))) ; theorem :: RELAT_1:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: RELAT_1:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")))))) ; theorem :: RELAT_1:64 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:66 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X"))) ")" ))) ; theorem :: RELAT_1:67 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: RELAT_1:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))))) ; registrationlet "R" be ($#m1_hidden :::"Relation":::); reduce ; end; theorem :: RELAT_1:69 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R")))) ; theorem :: RELAT_1:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:71 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; reduce ; end; theorem :: RELAT_1:72 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:73 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:74 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:75 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:76 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:77 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:78 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:79 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:80 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ))))) ; registrationlet "R" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:81 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: RELAT_1:82 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: RELAT_1:83 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))))) ; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); func "Y" :::"|`"::: "R" -> ($#m1_hidden :::"Relation":::) means :: RELAT_1:def 12 (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"::: ) it) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" )); end; :: deftheorem defines :::"|`"::: RELAT_1:def 12 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))) "iff" (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 "b3"))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" )) ")" ))); registrationlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k6_relat_1 :::"|`"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:84 (Bool "for" (Set (Var "y")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) ")" ) ")" ))) ; theorem :: RELAT_1:85 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))) ; theorem :: RELAT_1:86 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:87 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:88 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:89 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))))) ; theorem :: RELAT_1:90 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")))))) ; theorem :: RELAT_1:91 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:92 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:93 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: RELAT_1:94 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))))) ; registrationlet "R" be ($#m1_hidden :::"Relation":::); reduce ; end; theorem :: RELAT_1:95 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R")))) ; theorem :: RELAT_1:96 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))))) ; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); reduce ; end; theorem :: RELAT_1:97 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:98 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:99 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:100 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:101 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P2")))))) ; theorem :: RELAT_1:102 (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "Y1")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y2")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P2")))))) ; theorem :: RELAT_1:103 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ))))) ; theorem :: RELAT_1:104 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ))))) ; theorem :: RELAT_1:105 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ))))) ; theorem :: RELAT_1:106 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: RELAT_1:107 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: RELAT_1:108 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ))))) ; theorem :: RELAT_1:109 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; func "R" :::".:"::: "X" -> ($#m1_hidden :::"set"::: ) means :: RELAT_1:def 13 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") ")" )) ")" )); end; :: deftheorem defines :::".:"::: RELAT_1:def 13 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (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 "X"))) ")" )) ")" )) ")" ))); theorem :: RELAT_1:110 (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 (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (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 "X"))) ")" )) ")" ))) ; theorem :: RELAT_1:111 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:112 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")) ")" ))))) ; theorem :: RELAT_1:113 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:114 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ))))) ; theorem :: RELAT_1:115 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))))) ; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "R" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:116 canceled; theorem :: RELAT_1:117 canceled; theorem :: RELAT_1:118 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X"))) ")" ))) ; theorem :: RELAT_1:119 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: RELAT_1:120 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:121 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:122 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:123 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:124 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "P")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:125 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "P")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:126 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "P")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ))))) ; theorem :: RELAT_1:127 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P")) ")" )))) ; theorem :: RELAT_1:128 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:129 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:130 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "Y" be ($#m1_hidden :::"set"::: ) ; func "R" :::"""::: "Y" -> ($#m1_hidden :::"set"::: ) means :: RELAT_1:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "Y") ")" )) ")" )); end; :: deftheorem defines :::"""::: RELAT_1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" )) ")" ))); theorem :: RELAT_1:131 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" ))) ; theorem :: RELAT_1:132 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))))) ; theorem :: RELAT_1:133 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:134 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) ; theorem :: RELAT_1:135 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ))))) ; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "Y" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k8_relat_1 :::"""::: ) "Y") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "R" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Relation":::); let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k8_relat_1 :::"""::: ) "Y") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RELAT_1:136 canceled; theorem :: RELAT_1:137 canceled; theorem :: RELAT_1:138 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) ")" ))) ; theorem :: RELAT_1:139 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: RELAT_1:140 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:141 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:142 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "X")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:143 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:144 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "P")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:145 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "P")) ($#k8_relat_1 :::"""::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")))))) ; theorem :: RELAT_1:146 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; theorem :: RELAT_1:147 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )))) ; theorem :: RELAT_1:148 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; begin definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"empty-yielding"::: means :: RELAT_1:def 15 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"empty-yielding"::: RELAT_1:def 15 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_relat_1 :::"empty-yielding"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" )); theorem :: RELAT_1:149 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_relat_1 :::"empty-yielding"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ; theorem :: RELAT_1:150 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RELAT_1:151 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:152 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: RELAT_1:153 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; theorem :: RELAT_1:154 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )))) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v3_relat_1 :::"empty-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#v3_relat_1 :::"empty-yielding"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v3_relat_1 :::"empty-yielding"::: ) ; end; theorem :: RELAT_1:155 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Bool "not" (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) "is" ($#v3_relat_1 :::"empty-yielding"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "R")) "is" ($#v3_relat_1 :::"empty-yielding"::: ) )))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; func :::"Im"::: "(" "R" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: RELAT_1:def 16 (Set "R" ($#k7_relat_1 :::".:"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"Im"::: RELAT_1:def 16 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))); scheme :: RELAT_1:sch 2 ExtensionalityR{ F1() -> ($#m1_hidden :::"Relation":::), F2() -> ($#m1_hidden :::"Relation":::), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool (Set F1 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "iff" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]) ")" )) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) "iff" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]) ")" )) proof end; theorem :: RELAT_1:156 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:157 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")) ")" ))))) ; theorem :: RELAT_1:158 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ; theorem :: RELAT_1:159 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ; theorem :: RELAT_1:160 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" )) ; theorem :: RELAT_1:161 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) ; theorem :: RELAT_1:162 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) ; theorem :: RELAT_1:163 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Q"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "Q")) ")" )))) ; theorem :: RELAT_1:164 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Q"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "Q")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S")) ")" )))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; func :::"Coim"::: "(" "R" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: RELAT_1:def 17 (Set "R" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"Coim"::: RELAT_1:def 17 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))); registrationlet "R" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "R") -> ($#v1_zfmisc_1 :::"trivial"::: ) ; end; registrationlet "R" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v1_zfmisc_1 :::"trivial"::: ) ; end; theorem :: RELAT_1:165 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "S")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S")))))) ; theorem :: RELAT_1:166 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Q")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Set (Var "Q")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "Q")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); attr "R" is "X" :::"-defined"::: means :: RELAT_1:def 18 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "R") ($#r1_tarski :::"c="::: ) "X"); attr "R" is "X" :::"-valued"::: means :: RELAT_1:def 19 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") ($#r1_tarski :::"c="::: ) "X"); end; :: deftheorem defines :::"-defined"::: RELAT_1:def 18 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" (Set (Var "X")) ($#v4_relat_1 :::"-defined"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))); :: deftheorem defines :::"-valued"::: RELAT_1:def 19 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" (Set (Var "X")) ($#v5_relat_1 :::"-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))); registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: RELAT_1:167 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; registrationlet "X", "A" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "A")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> "A" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X", "A" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "A")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> "X" ($#v4_relat_1 :::"-defined"::: ) "A" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "A")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "S" ($#k3_relat_1 :::"(#)"::: ) "R") -> "A" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "A")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"(#)"::: ) "S") -> "A" ($#v4_relat_1 :::"-defined"::: ) ; end; theorem :: RELAT_1:168 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) ; theorem :: RELAT_1:169 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" )) ")" ))) ; theorem :: RELAT_1:170 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) "iff" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: RELAT_1:171 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" (Set (Var "X")) ($#v4_relat_1 :::"-defined"::: ) ) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" (Set (Var "Y")) ($#v5_relat_1 :::"-valued"::: ) ) ")" )) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_relat_1 :::"non-empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); cluster -> "X" ($#v4_relat_1 :::"-defined"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; theorem :: RELAT_1:172 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: RELAT_1:173 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); reduce ; end; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); reduce ; end; theorem :: RELAT_1:174 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; theorem :: RELAT_1:175 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))))))) ; theorem :: RELAT_1:176 (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" ))))) ; theorem :: RELAT_1:177 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")))))) ; theorem :: RELAT_1:178 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ))))) ; theorem :: RELAT_1:179 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "R")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "S")))) ; theorem :: RELAT_1:180 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "R")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "S")))) ; theorem :: RELAT_1:181 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: RELAT_1:182 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "R")) "is" (Set (Var "Y")) ($#v4_relat_1 :::"-defined"::: ) ))) ; theorem :: RELAT_1:183 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "R")) "is" (Set (Var "Y")) ($#v5_relat_1 :::"-valued"::: ) ))) ; theorem :: RELAT_1:184 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) "iff" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ))) ")" )) ; theorem :: RELAT_1:185 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: RELAT_1:186 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))))) ; registrationlet "A", "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "A")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "X" ($#k6_relat_1 :::"|`"::: ) "R") -> "A" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X", "A" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "A")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "X" ($#k6_relat_1 :::"|`"::: ) "R") -> "X" ($#v5_relat_1 :::"-valued"::: ) "A" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) -> ($#v1_xboole_0 :::"empty"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) -> ($#v1_xboole_0 :::"empty"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end;