:: RELAT_2  semantic presentation begin  












definitionlet "R" be   ($#m1_hidden :::"Relation":::); let "X" be    ($#m1_hidden :::"set"::: )  ; pred "R" :::"is_reflexive_in"::: "X" means :: RELAT_2:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); pred "R" :::"is_irreflexive_in"::: "X" means :: RELAT_2:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R"))); pred "R" :::"is_symmetric_in"::: "X" means :: RELAT_2:def 3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); pred "R" :::"is_antisymmetric_in"::: "X" means :: RELAT_2:def 4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))); pred "R" :::"is_asymmetric_in"::: "X" means :: RELAT_2:def 5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R"))); pred "R" :::"is_connected_in"::: "X" means :: RELAT_2:def 6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R"))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); pred "R" :::"is_strongly_connected_in"::: "X" means :: RELAT_2:def 7 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R"))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); pred "R" :::"is_transitive_in"::: "X" means :: RELAT_2:def 8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); end; 








































:: deftheorem    defines :::"is_reflexive_in"::: RELAT_2:def 1 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r1_relat_2 :::"is_reflexive_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" ))); 
 
:: deftheorem    defines :::"is_irreflexive_in"::: RELAT_2:def 2 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_relat_2 :::"is_irreflexive_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))))  ")" ))); 
 
:: deftheorem    defines :::"is_symmetric_in"::: RELAT_2:def 3 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r3_relat_2 :::"is_symmetric_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" ))); 
 
:: deftheorem    defines :::"is_antisymmetric_in"::: RELAT_2:def 4 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))  ")" ))); 
 
:: deftheorem    defines :::"is_asymmetric_in"::: RELAT_2:def 5 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r5_relat_2 :::"is_asymmetric_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))))  ")" ))); 
 
:: deftheorem    defines :::"is_connected_in"::: RELAT_2:def 6 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r6_relat_2 :::"is_connected_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" ))); 
 
:: deftheorem    defines :::"is_strongly_connected_in"::: RELAT_2:def 7 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r7_relat_2 :::"is_strongly_connected_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" ))); 
 
:: deftheorem    defines :::"is_transitive_in"::: RELAT_2:def 8 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r8_relat_2 :::"is_transitive_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" ))); 
 definitionlet "R" be   ($#m1_hidden :::"Relation":::); attr "R" is  :::"reflexive":::  means :: RELAT_2:def 9 (Bool "R"  ($#r1_relat_2 :::"is_reflexive_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"irreflexive":::  means :: RELAT_2:def 10 (Bool "R"  ($#r2_relat_2 :::"is_irreflexive_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"symmetric":::  means :: RELAT_2:def 11 (Bool "R"  ($#r3_relat_2 :::"is_symmetric_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"antisymmetric":::  means :: RELAT_2:def 12 (Bool "R"  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"asymmetric":::  means :: RELAT_2:def 13 (Bool "R"  ($#r5_relat_2 :::"is_asymmetric_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"connected":::  means :: RELAT_2:def 14 (Bool "R"  ($#r6_relat_2 :::"is_connected_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"strongly_connected":::  means :: RELAT_2:def 15 (Bool "R"  ($#r7_relat_2 :::"is_strongly_connected_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); attr "R" is  :::"transitive":::  means :: RELAT_2:def 16 (Bool "R"  ($#r8_relat_2 :::"is_transitive_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")); end; 
































:: deftheorem    defines :::"reflexive"::: RELAT_2:def 9 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_relat_2 :::"reflexive"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r1_relat_2 :::"is_reflexive_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"irreflexive"::: RELAT_2:def 10 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v2_relat_2 :::"irreflexive"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r2_relat_2 :::"is_irreflexive_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"symmetric"::: RELAT_2:def 11 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v3_relat_2 :::"symmetric"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r3_relat_2 :::"is_symmetric_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"antisymmetric"::: RELAT_2:def 12 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"asymmetric"::: RELAT_2:def 13 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v5_relat_2 :::"asymmetric"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r5_relat_2 :::"is_asymmetric_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"connected"::: RELAT_2:def 14 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r6_relat_2 :::"is_connected_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"strongly_connected"::: RELAT_2:def 15 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v7_relat_2 :::"strongly_connected"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r7_relat_2 :::"is_strongly_connected_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 
:: deftheorem    defines :::"transitive"::: RELAT_2:def 16 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v8_relat_2 :::"transitive"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r8_relat_2 :::"is_transitive_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )); 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )     ($#v1_relat_1 :::"Relation-like"::: )    ->   ($#v1_relat_2 :::"reflexive"::: )     ($#v2_relat_2 :::"irreflexive"::: )     ($#v3_relat_2 :::"symmetric"::: )     ($#v4_relat_2 :::"antisymmetric"::: )     ($#v5_relat_2 :::"asymmetric"::: )     ($#v6_relat_2 :::"connected"::: )     ($#v7_relat_2 :::"strongly_connected"::: )     ($#v8_relat_2 :::"transitive"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: RELAT_2:1 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_relat_2 :::"reflexive"::: )  ) "iff" (Bool (Set   ($#k4_relat_1 :::"id"::: )  (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "R")))  ")" )) ; 
 
theorem :: RELAT_2:2 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v2_relat_2 :::"irreflexive"::: )  ) "iff" (Bool (Set   ($#k4_relat_1 :::"id"::: )  (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "R")))  ")" )) ; 
 
theorem :: RELAT_2:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "R"))  ($#k4_xboole_0 :::"\"::: )  (Set  "("  ($#k4_relat_1 :::"id"::: )  (Set (Var "X")) ")" ))  ($#r5_relat_2 :::"is_asymmetric_in"::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: RELAT_2:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R"))  ($#r5_relat_2 :::"is_asymmetric_in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k4_relat_1 :::"id"::: )  (Set (Var "X")) ")" ))  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set (Var "X"))))) ; 
 
theorem :: RELAT_2:5 canceled; 
 
theorem :: RELAT_2:6 canceled; 
 
theorem :: RELAT_2:7 canceled; 
 
theorem :: RELAT_2:8 canceled; 
 
theorem :: RELAT_2:9 canceled; 
 
theorem :: RELAT_2:10 canceled; 
 
theorem :: RELAT_2:11 canceled; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v3_relat_2 :::"symmetric"::: )     ($#v8_relat_2 :::"transitive"::: )    ->   ($#v1_relat_2 :::"reflexive"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_relat_1 :::"id"::: )  "X") ->   ($#v3_relat_2 :::"symmetric"::: )     ($#v4_relat_2 :::"antisymmetric"::: )     ($#v8_relat_2 :::"transitive"::: )   ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_2 :::"irreflexive"::: )     ($#v8_relat_2 :::"transitive"::: )    ->   ($#v5_relat_2 :::"asymmetric"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v5_relat_2 :::"asymmetric"::: )    ->   ($#v2_relat_2 :::"irreflexive"::: )     ($#v4_relat_2 :::"antisymmetric"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "R" be   ($#v1_relat_2 :::"reflexive"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "R"  ($#k2_relat_1 :::"~"::: )  ) ->   ($#v1_relat_2 :::"reflexive"::: )   ; 
end; registrationlet "R" be   ($#v2_relat_2 :::"irreflexive"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "R"  ($#k2_relat_1 :::"~"::: )  ) ->   ($#v2_relat_2 :::"irreflexive"::: )   ; 
end; 
theorem :: RELAT_2:12 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v1_relat_2 :::"reflexive"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ")" ))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ")" )))  ")" )) ; 
 
theorem :: RELAT_2:13 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v3_relat_2 :::"symmetric"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ))  ")" )) ; 
 registrationlet "P", "R" be   ($#v1_relat_2 :::"reflexive"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k2_xboole_0 :::"\/"::: )  "R") ->   ($#v1_relat_2 :::"reflexive"::: )   ; 

cluster (Set "P"  ($#k3_xboole_0 :::"/\"::: )  "R") ->   ($#v1_relat_2 :::"reflexive"::: )   ; 
end; registrationlet "P", "R" be   ($#v2_relat_2 :::"irreflexive"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k2_xboole_0 :::"\/"::: )  "R") ->   ($#v2_relat_2 :::"irreflexive"::: )   ; 

cluster (Set "P"  ($#k3_xboole_0 :::"/\"::: )  "R") ->   ($#v2_relat_2 :::"irreflexive"::: )   ; 
end; registrationlet "P" be   ($#v2_relat_2 :::"irreflexive"::: )    ($#m1_hidden :::"Relation":::); let "R" be   ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k4_xboole_0 :::"\"::: )  "R") ->   ($#v2_relat_2 :::"irreflexive"::: )   ; 
end; registrationlet "R" be   ($#v3_relat_2 :::"symmetric"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "R"  ($#k2_relat_1 :::"~"::: )  ) ->   ($#v3_relat_2 :::"symmetric"::: )   ; 
end; registrationlet "P", "R" be   ($#v3_relat_2 :::"symmetric"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k2_xboole_0 :::"\/"::: )  "R") ->   ($#v3_relat_2 :::"symmetric"::: )   ; 

cluster (Set "P"  ($#k3_xboole_0 :::"/\"::: )  "R") ->   ($#v3_relat_2 :::"symmetric"::: )   ; 

cluster (Set "P"  ($#k4_xboole_0 :::"\"::: )  "R") ->   ($#v3_relat_2 :::"symmetric"::: )   ; 
end; registrationlet "R" be   ($#v5_relat_2 :::"asymmetric"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "R"  ($#k2_relat_1 :::"~"::: )  ) ->   ($#v5_relat_2 :::"asymmetric"::: )   ; 
end; registrationlet "P" be   ($#m1_hidden :::"Relation":::); let "R" be   ($#v5_relat_2 :::"asymmetric"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k3_xboole_0 :::"/\"::: )  "R") ->   ($#v5_relat_2 :::"asymmetric"::: )   ; 

cluster (Set "R"  ($#k3_xboole_0 :::"/\"::: )  "P") ->   ($#v5_relat_2 :::"asymmetric"::: )   ; 
end; registrationlet "P" be   ($#v5_relat_2 :::"asymmetric"::: )    ($#m1_hidden :::"Relation":::); let "R" be   ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k4_xboole_0 :::"\"::: )  "R") ->   ($#v5_relat_2 :::"asymmetric"::: )   ; 
end; 
theorem :: RELAT_2:14 canceled; 
 
theorem :: RELAT_2:15 canceled; 
 
theorem :: RELAT_2:16 canceled; 
 
theorem :: RELAT_2:17 canceled; 
 
theorem :: RELAT_2:18 canceled; 
 
theorem :: RELAT_2:19 canceled; 
 
theorem :: RELAT_2:20 canceled; 
 
theorem :: RELAT_2:21 canceled; 
 
theorem :: RELAT_2:22 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  ) "iff" (Bool (Set (Set (Var "R"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_relat_1 :::"id"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "R")) ")" )))  ")" )) ; 
 registrationlet "R" be   ($#v4_relat_2 :::"antisymmetric"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "R"  ($#k2_relat_1 :::"~"::: )  ) ->   ($#v4_relat_2 :::"antisymmetric"::: )   ; 
end; registrationlet "P" be   ($#v4_relat_2 :::"antisymmetric"::: )    ($#m1_hidden :::"Relation":::); let "R" be   ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k3_xboole_0 :::"/\"::: )  "R") ->   ($#v4_relat_2 :::"antisymmetric"::: )   ; 

cluster (Set "R"  ($#k3_xboole_0 :::"/\"::: )  "P") ->   ($#v4_relat_2 :::"antisymmetric"::: )   ; 

cluster (Set "P"  ($#k4_xboole_0 :::"\"::: )  "R") ->   ($#v4_relat_2 :::"antisymmetric"::: )   ; 
end; registrationlet "R" be   ($#v8_relat_2 :::"transitive"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "R"  ($#k2_relat_1 :::"~"::: )  ) ->   ($#v8_relat_2 :::"transitive"::: )   ; 
end; registrationlet "P", "R" be   ($#v8_relat_2 :::"transitive"::: )    ($#m1_hidden :::"Relation":::); 
cluster (Set "P"  ($#k3_xboole_0 :::"/\"::: )  "R") ->   ($#v8_relat_2 :::"transitive"::: )   ; 
end; 
theorem :: RELAT_2:23 canceled; 
 
theorem :: RELAT_2:24 canceled; 
 
theorem :: RELAT_2:25 canceled; 
 
theorem :: RELAT_2:26 canceled; 
 
theorem :: RELAT_2:27 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v8_relat_2 :::"transitive"::: )  ) "iff" (Bool (Set (Set (Var "R"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set (Var "R")))  ")" )) ; 
 
theorem :: RELAT_2:28 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )  ) "iff" (Bool (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ) "," (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  "("  ($#k4_relat_1 :::"id"::: )  (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "R"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ")" )))  ")" )) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v7_relat_2 :::"strongly_connected"::: )    ->   ($#v1_relat_2 :::"reflexive"::: )     ($#v6_relat_2 :::"connected"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: RELAT_2:29 canceled; 
 
theorem :: RELAT_2:30 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v7_relat_2 :::"strongly_connected"::: )  ) "iff" (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ) "," (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ")" )))  ")" )) ; 
 
theorem :: RELAT_2:31 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v8_relat_2 :::"transitive"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "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  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" )) ;