:: WELLORD1  semantic presentation begin  
















definitionlet "R" be   ($#m1_hidden :::"Relation":::); let "a" be    ($#m1_hidden :::"set"::: )  ; func "R" :::"-Seg"::: "a" ->    ($#m1_hidden :::"set"::: )   equals :: WELLORD1:def 1 (Set (Set  "("  ($#k10_relat_1 :::"Coim"::: )   "(" "R" "," "a" ")"  ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) )); end; 






:: deftheorem    defines :::"-Seg"::: WELLORD1:def 1 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_relat_1 :::"Coim"::: )   "(" (Set (Var "R")) "," (Set (Var "a")) ")"  ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))))); 
 
theorem :: WELLORD1:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "a")) "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"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" ))) ; 
 
theorem :: WELLORD1:2 (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   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) "or" (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ))) ; 
 definitionlet "R" be   ($#m1_hidden :::"Relation":::); attr "R" is  :::"well_founded":::  means :: WELLORD1:def 2 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set "R"  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))  ")" ))); let "X" be    ($#m1_hidden :::"set"::: )  ; pred "R" :::"is_well_founded_in"::: "X" means :: WELLORD1:def 3 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  "X") & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set "R"  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))  ")" ))); end; 









:: deftheorem    defines :::"well_founded"::: WELLORD1:def 2 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellord1 :::"well_founded"::: )  ) "iff" (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))  ")" )))  ")" )); 
 
:: deftheorem    defines :::"is_well_founded_in"::: WELLORD1: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"))  ($#r1_wellord1 :::"is_well_founded_in"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))  ")" )))  ")" ))); 
 
theorem :: WELLORD1:3 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellord1 :::"well_founded"::: )  ) "iff" (Bool (Set (Var "R"))  ($#r1_wellord1 :::"is_well_founded_in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))  ")" )) ; 
 definitionlet "R" be   ($#m1_hidden :::"Relation":::); attr "R" is  :::"well-ordering":::  means :: WELLORD1:def 4 (Bool  "("  (Bool "R" "is"   ($#v1_relat_2 :::"reflexive"::: )  ) & (Bool "R" "is"   ($#v8_relat_2 :::"transitive"::: )  ) & (Bool "R" "is"   ($#v4_relat_2 :::"antisymmetric"::: )  ) & (Bool "R" "is"   ($#v6_relat_2 :::"connected"::: )  ) & (Bool "R" "is"   ($#v1_wellord1 :::"well_founded"::: )  )  ")" ); let "X" be    ($#m1_hidden :::"set"::: )  ; pred "R" :::"well_orders"::: "X" means :: WELLORD1:def 5 (Bool  "("  (Bool "R"  ($#r1_relat_2 :::"is_reflexive_in"::: )  "X") & (Bool "R"  ($#r8_relat_2 :::"is_transitive_in"::: )  "X") & (Bool "R"  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  "X") & (Bool "R"  ($#r6_relat_2 :::"is_connected_in"::: )  "X") & (Bool "R"  ($#r1_wellord1 :::"is_well_founded_in"::: )  "X")  ")" ); end; 









:: deftheorem    defines :::"well-ordering"::: WELLORD1:def 4 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_relat_2 :::"reflexive"::: )  ) & (Bool (Set (Var "R")) "is"   ($#v8_relat_2 :::"transitive"::: )  ) & (Bool (Set (Var "R")) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  ) & (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )  ) & (Bool (Set (Var "R")) "is"   ($#v1_wellord1 :::"well_founded"::: )  )  ")" )  ")" )); 
 
:: deftheorem    defines :::"well_orders"::: WELLORD1: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"))  ($#r2_wellord1 :::"well_orders"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "R"))  ($#r1_relat_2 :::"is_reflexive_in"::: )  (Set (Var "X"))) & (Bool (Set (Var "R"))  ($#r8_relat_2 :::"is_transitive_in"::: )  (Set (Var "X"))) & (Bool (Set (Var "R"))  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set (Var "X"))) & (Bool (Set (Var "R"))  ($#r6_relat_2 :::"is_connected_in"::: )  (Set (Var "X"))) & (Bool (Set (Var "R"))  ($#r1_wellord1 :::"is_well_founded_in"::: )  (Set (Var "X")))  ")" )  ")" ))); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_wellord1 :::"well-ordering"::: )    ->   ($#v1_relat_2 :::"reflexive"::: )     ($#v4_relat_2 :::"antisymmetric"::: )     ($#v6_relat_2 :::"connected"::: )     ($#v8_relat_2 :::"transitive"::: )     ($#v1_wellord1 :::"well_founded"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_relat_2 :::"reflexive"::: )     ($#v4_relat_2 :::"antisymmetric"::: )     ($#v6_relat_2 :::"connected"::: )     ($#v8_relat_2 :::"transitive"::: )     ($#v1_wellord1 :::"well_founded"::: )    ->   ($#v2_wellord1 :::"well-ordering"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: WELLORD1:4 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_wellord1 :::"well_orders"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) "iff" (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )  ")" )) ; 
 
theorem :: WELLORD1:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R"))  ($#r2_wellord1 :::"well_orders"::: )  (Set (Var "X")))) "holds"  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" ))))) ; 
 
theorem :: WELLORD1:6 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" )))) ; 
 
theorem :: WELLORD1:7 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" ))) ; 
 
theorem :: WELLORD1:8 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) "or" (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "or" (Bool  "ex" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Bool  "not" (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" ))  ")" ))) ; 
 




theorem :: WELLORD1:9 (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))))) ; 
 definitionlet "R" be   ($#m1_hidden :::"Relation":::); let "Y" be    ($#m1_hidden :::"set"::: )  ; func "R" :::"|_2"::: "Y" ->   ($#m1_hidden :::"Relation":::) equals :: WELLORD1:def 6 (Set "R"  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "Y" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; 






:: deftheorem    defines :::"|_2"::: WELLORD1:def 6 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))))); 
 
theorem :: WELLORD1:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k6_relat_1 :::"|`"::: )  (Set (Var "R")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))))) ; 
 
theorem :: WELLORD1:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k6_relat_1 :::"|`"::: )  (Set  "(" (Set (Var "R"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: WELLORD1:12 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: WELLORD1:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: WELLORD1:14 (Bool  "for" (Set (Var "X")) "," (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" )  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))))) ; 
 
theorem :: WELLORD1:15 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v1_relat_2 :::"reflexive"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X"))) "is"   ($#v1_relat_2 :::"reflexive"::: )  ))) ; 
 
theorem :: WELLORD1:16 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y"))) "is"   ($#v6_relat_2 :::"connected"::: )  ))) ; 
 
theorem :: WELLORD1:17 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v8_relat_2 :::"transitive"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y"))) "is"   ($#v8_relat_2 :::"transitive"::: )  ))) ; 
 
theorem :: WELLORD1:18 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y"))) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  ))) ; 
 
theorem :: WELLORD1:19 (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"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: WELLORD1:20 (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"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")) ")" )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")))))) ; 
 
theorem :: WELLORD1:21 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")) ")" )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))))) ; 
 
theorem :: WELLORD1:22 (Bool  "for" (Set (Var "Z")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")) ")" )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Z")))))) ; 
 
theorem :: WELLORD1:23 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "R")))) ; 
 
theorem :: WELLORD1:24 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v1_wellord1 :::"well_founded"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X"))) "is"   ($#v1_wellord1 :::"well_founded"::: )  ))) ; 
 
theorem :: WELLORD1:25 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y"))) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ))) ; 
 
theorem :: WELLORD1:26 (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 (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a"))) "," (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  ))) ; 
 
theorem :: WELLORD1:27 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")))))) ; 
 
theorem :: WELLORD1:28 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) "or" (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a"))))  ")" ))  ")" ) "iff" (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))))  ")" ))) ; 
 
theorem :: WELLORD1:29 (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 (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (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"))))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) "iff" (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b"))))  ")" ))) ; 
 
theorem :: WELLORD1:30 (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 (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (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"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b"))))  ")" )  ")" ))) ; 
 
theorem :: WELLORD1:31 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: WELLORD1:32 (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))))) ; 
 
theorem :: WELLORD1:33 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" )) "holds"  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))))) ; 
 
theorem :: WELLORD1:34 (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 (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (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")))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a"))))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))  ")" )  ")" )) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))) ; 
 
theorem :: WELLORD1:35 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (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 "R"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))))) ; 
 definitionlet "R", "S" be   ($#m1_hidden :::"Relation":::); let "F" be   ($#m1_hidden :::"Function":::); pred "F" :::"is_isomorphism_of"::: "R" "," "S" means :: WELLORD1:def 7 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "F")  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "F")  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  "S")) & (Bool "F" "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (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"::: )  "R") "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  "R")) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "S")  ")" )  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_isomorphism_of"::: WELLORD1:def 7 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "S")))) & (Bool (Set (Var "F")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (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 "R"))) "iff" (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")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "S")))  ")" )  ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: WELLORD1:36 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (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 "R"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))  ")" )))) ; 
 definitionlet "R", "S" be   ($#m1_hidden :::"Relation":::); pred "R" "," "S" :::"are_isomorphic":::  means :: WELLORD1:def 8 (Bool  "ex" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  "R" "," "S")); end; 





:: deftheorem    defines :::"are_isomorphic"::: WELLORD1:def 8 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S"))))  ")" )); 
 
theorem :: WELLORD1:37 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set   ($#k4_relat_1 :::"id"::: )  (Set  "("  ($#k1_relat_1 :::"field"::: )  (Set (Var "R")) ")" ))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "R")))) ; 
 
theorem :: WELLORD1:38 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Var "R")) "," (Set (Var "R"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: WELLORD1:39 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k2_funct_1 :::"""::: )  )  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "S")) "," (Set (Var "R"))))) ; 
 
theorem :: WELLORD1:40 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "S")) "," (Set (Var "R"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: WELLORD1:41 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S"))) & (Bool (Set (Var "G"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "S")) "," (Set (Var "T")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "F")))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "T"))))) ; 
 
theorem :: WELLORD1:42 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "R")) "," (Set (Var "T"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: WELLORD1:43 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "R")) "is"   ($#v1_relat_2 :::"reflexive"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v1_relat_2 :::"reflexive"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "R")) "is"   ($#v8_relat_2 :::"transitive"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v8_relat_2 :::"transitive"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v6_relat_2 :::"connected"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "R")) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v4_relat_2 :::"antisymmetric"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "R")) "is"   ($#v1_wellord1 :::"well_founded"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v1_wellord1 :::"well_founded"::: )  )  ")"   ")" ))) ; 
 
theorem :: WELLORD1:44 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ))) ; 
 
theorem :: WELLORD1:45 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S"))) & (Bool (Set (Var "G"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))))) ; 
 definitionlet "R", "S" be   ($#m1_hidden :::"Relation":::); assume that  
(Bool (Set (Const "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )
 and  
(Bool (Set (Const "R")) "," (Set (Const "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )
 ; func  :::"canonical_isomorphism_of":::  "(" "R" "," "S" ")"  ->   ($#m1_hidden :::"Function":::) means :: WELLORD1:def 9 (Bool it  ($#r3_wellord1 :::"is_isomorphism_of"::: )  "R" "," "S"); end; 







:: deftheorem    defines :::"canonical_isomorphism_of"::: WELLORD1:def 9 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "R")) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set (Var "R")) "," (Set (Var "S")) ")" )) "iff" (Bool (Set (Var "b3"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))  ")" ))); 
 
theorem :: WELLORD1:46 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool  "not" (Bool (Set (Var "R")) "," (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  )))) ; 
 
theorem :: WELLORD1:47 (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 (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (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")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "not" (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" )) "," (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  )))) ; 
 
theorem :: WELLORD1:48 (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Z")))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Z"))) "," (Set (Set (Var "S"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "F"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "Z")) ")" ))) & (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Z"))) "," (Set (Set (Var "S"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "F"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "Z")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" )))) ; 
 
theorem :: WELLORD1:49 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool  "ex" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "S")))) & (Bool (Set (Set (Var "F"))  ($#k7_relat_1 :::".:"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b"))))  ")" ))))) ; 
 
theorem :: WELLORD1:50 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "F"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set (Var "R")) "," (Set (Var "S")))) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool  "ex" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "S")))) & (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" )) "," (Set (Set (Var "S"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" ))))) ; 
 
theorem :: WELLORD1:51 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (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 "S")))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "S")))) & (Bool (Set (Var "R")) "," (Set (Set (Var "S"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  ) & (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" )) "," (Set (Set (Var "S"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "c")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "c")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "b")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "S")))  ")" ))) ; 
 
theorem :: WELLORD1:52 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Bool  "not" (Set (Var "R")) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) "or"  "not" (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" )) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" )  ")" )) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "S")))) & (Bool (Set (Var "R")) "," (Set (Set (Var "S"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "S"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" ))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" ))) ; 
 
theorem :: WELLORD1:53 (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   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Bool  "not" (Set (Var "R")) "," (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) & (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" )) "," (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" )))) ; 
 
theorem :: WELLORD1:54 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "," (Set (Var "S"))  ($#r4_wellord1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) ;