:: SYSREL semantic presentation begin theorem :: SYSREL:1 (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 ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: SYSREL:2 (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 ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))))) ; theorem :: SYSREL:3 (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_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: SYSREL:4 (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_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: SYSREL:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: SYSREL:6 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "S")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "T")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "T")) ")" )))) ; theorem :: SYSREL:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (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")))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (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")))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (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 "Y")))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (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 "X")))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) ")" ")" ))) ; theorem :: SYSREL:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Set (Var "Z")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ))) ; theorem :: SYSREL:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Z")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Z")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "W")) ")" ))))) ; theorem :: SYSREL:10 (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"))) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )))) "holds" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: SYSREL:11 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k2_relat_1 :::"~"::: ) ))) ; theorem :: SYSREL:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))))) ; theorem :: SYSREL:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SYSREL:14 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" ))) ")" )) ; theorem :: SYSREL:15 (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 ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "Y"))))) ; theorem :: SYSREL:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SYSREL:17 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )))) ; theorem :: SYSREL:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )))) "holds" (Bool "(" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) ")" ))) ; theorem :: SYSREL:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )))) ; theorem :: SYSREL:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ))) ")" ))) ; theorem :: SYSREL:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")))) ")" ")" ))) ; theorem :: SYSREL:22 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" & "(" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" ")" )) ; theorem :: SYSREL:23 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ))) ")" ")" )) ; theorem :: SYSREL:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); func :::"CL"::: "R" -> ($#m1_hidden :::"Relation":::) equals :: SYSREL:def 1 (Set "R" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "R" ")" ) ")" )); end; :: deftheorem defines :::"CL"::: SYSREL:def 1 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" )))); theorem :: SYSREL:25 (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 ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: SYSREL:26 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )))) ; theorem :: SYSREL:27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )))) "implies" (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 "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" & "(" (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 "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )))) "implies" (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 "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" & "(" (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 "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" ")" ))) ; theorem :: SYSREL:28 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )))) ; theorem :: SYSREL:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" ) ")" ")" ))) ; theorem :: SYSREL:30 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ))) ")" ) ")" ")" ))) ; theorem :: SYSREL:31 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) ")" ) ")" ")" )) ; theorem :: SYSREL:32 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) ")" )) ; theorem :: SYSREL:33 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ))) & (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ))) ")" )) ; theorem :: SYSREL:34 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" )) ; theorem :: SYSREL:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (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 "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))) ")" ")" ))) ; theorem :: SYSREL:36 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) & (Bool (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ))) ")" ) ")" ")" )) ; theorem :: SYSREL:37 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )) ; theorem :: SYSREL:38 (Bool "for" (Set (Var "S")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )) ; theorem :: SYSREL:39 (Bool "for" (Set (Var "S")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R")))) ")" ")" )) ; theorem :: SYSREL:40 (Bool "for" (Set (Var "S")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "S")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sysrel :::"CL"::: ) (Set (Var "R")))) ")" ")" )) ;