:: WELLORD1 semantic presentation

begin

definition
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let a be ( ( ) ( ) set ) ;
func R -Seg a -> ( ( ) ( ) set ) equals :: WELLORD1:def 1
(Coim (R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,a : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) \ {a : ( ( ) ( ) set ) } : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool (Coim (R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,a : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: WELLORD1:1
for x, a being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( x : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) iff ( x : ( ( ) ( ) set ) <> a : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;

theorem :: WELLORD1:2
for x being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( x : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) or R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( ) set ) ) ;

definition
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr R is well_founded means :: WELLORD1:def 2
 for Y being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= field R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) );
let X be ( ( ) ( ) set ) ;
pred R is_well_founded_in X means :: WELLORD1:def 3
 for Y being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) );
end;

theorem :: WELLORD1:3
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( R : ( ( Relation-like ) ( Relation-like ) Relation) is well_founded iff R : ( ( Relation-like ) ( Relation-like ) Relation) is_well_founded_in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ;

definition
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr R is well-ordering means :: WELLORD1:def 4
( R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is reflexive & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is transitive & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is antisymmetric & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is connected & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is well_founded );
let X be ( ( ) ( ) set ) ;
pred R well_orders X means :: WELLORD1:def 5
( R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is_reflexive_in X : ( ( ) ( ) set ) & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is_transitive_in X : ( ( ) ( ) set ) & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is_antisymmetric_in X : ( ( ) ( ) set ) & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is_connected_in X : ( ( ) ( ) set ) & R : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is_well_founded_in X : ( ( ) ( ) set ) );
end;

registration
cluster Relation-like well-ordering -> Relation-like reflexive antisymmetric connected transitive well_founded for ( ( ) ( ) set ) ;
cluster Relation-like reflexive antisymmetric connected transitive well_founded -> Relation-like well-ordering for ( ( ) ( ) set ) ;
end;

theorem :: WELLORD1:4
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( R : ( ( Relation-like ) ( Relation-like ) Relation) well_orders field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) iff R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering ) ;

theorem :: WELLORD1:5
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) well_orders X : ( ( ) ( ) set ) holds
for Y being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & ( for b being ( ( ) ( ) set ) st b : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;

theorem :: WELLORD1:6
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
for Y being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & ( for b being ( ( ) ( ) set ) st b : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;

theorem :: WELLORD1:7
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & ( for b being ( ( ) ( ) set ) st b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;

theorem :: WELLORD1:8
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
for a being ( ( ) ( ) set ) holds
( not a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) or for b being ( ( ) ( ) set ) st b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
[b : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) or ex b being ( ( ) ( ) set ) st
( b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & ( for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [a : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & not c : ( ( ) ( ) set ) = a : ( ( ) ( ) set ) holds
[b : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ) ;

theorem :: WELLORD1:9
for a being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ;

definition
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let Y be ( ( ) ( ) set ) ;
func R |_2 Y -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: WELLORD1:def 6
R : ( ( ) ( ) set ) /\ [:Y : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ;
end;

theorem :: WELLORD1:10
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = (X : ( ( ) ( ) set ) |` R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: WELLORD1:11
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = X : ( ( ) ( ) set ) |` (R : ( ( Relation-like ) ( Relation-like ) Relation) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: WELLORD1:12
for x, X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st x : ( ( ) ( ) set ) in field (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ;

theorem :: WELLORD1:13
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( field (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & field (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ) ;

theorem :: WELLORD1:14
for X, a being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: WELLORD1:15
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is reflexive holds
R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) is reflexive ;

theorem :: WELLORD1:16
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is connected holds
R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) is connected ;

theorem :: WELLORD1:17
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is transitive holds
R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) is transitive ;

theorem :: WELLORD1:18
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is antisymmetric holds
R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) is antisymmetric ;

theorem :: WELLORD1:19
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:20
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:21
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:22
for Z, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st Z : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
(R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:23
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (field R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) = R : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:24
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well_founded holds
R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) is well_founded ;

theorem :: WELLORD1:25
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering ;

theorem :: WELLORD1:26
for a, b being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) are_c=-comparable ;

theorem :: WELLORD1:27
for b, a being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & b : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
(R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: WELLORD1:28
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & Y : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
( ( Y : ( ( ) ( ) set ) = field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) or ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) iff for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
for b being ( ( ) ( ) set ) st [b : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) holds
b : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) ) ;

theorem :: WELLORD1:29
for a, b being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
( [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) iff R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: WELLORD1:30
for a, b being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
( R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) iff ( a : ( ( ) ( ) set ) = b : ( ( ) ( ) set ) or a : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: WELLORD1:31
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & X : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
field (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ;

theorem :: WELLORD1:32
for a being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
field (R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: WELLORD1:33
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
for Z being ( ( ) ( ) set ) st ( for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
a : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) ) holds
field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ;

theorem :: WELLORD1:34
for a, b being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & ( for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
( [c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & c : ( ( ) ( ) set ) <> b : ( ( ) ( ) set ) ) ) holds
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:35
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & dom F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & rng F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & ( for a, b being ( ( ) ( ) set ) st [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & a : ( ( ) ( ) set ) <> b : ( ( ) ( ) set ) holds
( [(F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
[a : ( ( ) ( ) set ) ,(F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ;

definition
let R, S be ( ( Relation-like ) ( Relation-like ) Relation) ;
let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
pred F is_isomorphism_of R,S means :: WELLORD1:def 7
( dom F : ( ( ) ( ) Element of bool R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = field R : ( ( ) ( ) set ) : ( ( ) ( ) set ) & rng F : ( ( ) ( ) Element of bool R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = field S : ( ( ) ( ) set ) : ( ( ) ( ) set ) & F : ( ( ) ( ) Element of bool R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is one-to-one & ( for a, b being ( ( ) ( ) set ) holds
( [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) set ) iff ( a : ( ( ) ( ) set ) in field R : ( ( ) ( ) set ) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in field R : ( ( ) ( ) set ) : ( ( ) ( ) set ) & [(F : ( ( ) ( ) Element of bool R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(F : ( ( ) ( ) Element of bool R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in S : ( ( ) ( ) set ) ) ) ) );
end;

theorem :: WELLORD1:36
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
for a, b being ( ( ) ( ) set ) st [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & a : ( ( ) ( ) set ) <> b : ( ( ) ( ) set ) holds
( [(F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in S : ( ( Relation-like ) ( Relation-like ) Relation) & F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

definition
let R, S be ( ( Relation-like ) ( Relation-like ) Relation) ;
pred R,S are_isomorphic means :: WELLORD1:def 8
 ex F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ;
end;

theorem :: WELLORD1:37
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds id (field R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like field b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined field b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued Function-like one-to-one ) set ) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:38
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds R : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ;

theorem :: WELLORD1:39
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is_isomorphism_of S : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:40
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic holds
S : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ;

theorem :: WELLORD1:41
for R, S, T being ( ( Relation-like ) ( Relation-like ) Relation)
for F, G being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) & G : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of S : ( ( Relation-like ) ( Relation-like ) Relation) ,T : ( ( Relation-like ) ( Relation-like ) Relation) holds
G : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,T : ( ( Relation-like ) ( Relation-like ) Relation) ;

theorem :: WELLORD1:42
for R, S, T being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic & S : ( ( Relation-like ) ( Relation-like ) Relation) ,T : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic holds
R : ( ( Relation-like ) ( Relation-like ) Relation) ,T : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ;

theorem :: WELLORD1:43
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) is reflexive implies S : ( ( Relation-like ) ( Relation-like ) Relation) is reflexive ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) is transitive implies S : ( ( Relation-like ) ( Relation-like ) Relation) is transitive ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) is connected implies S : ( ( Relation-like ) ( Relation-like ) Relation) is connected ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) is antisymmetric implies S : ( ( Relation-like ) ( Relation-like ) Relation) is antisymmetric ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) is well_founded implies S : ( ( Relation-like ) ( Relation-like ) Relation) is well_founded ) ) ;

theorem :: WELLORD1:44
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
S : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering ;

theorem :: WELLORD1:45
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
for F, G being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) & G : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = G : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

definition
let R, S be ( ( Relation-like ) ( Relation-like ) Relation) ;
assume that
R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering and
R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ;
func canonical_isomorphism_of (R,S) -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: WELLORD1:def 9
it : ( ( ) ( ) Element of bool R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is_isomorphism_of R : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ;
end;

theorem :: WELLORD1:46
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
not R : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ;

theorem :: WELLORD1:47
for a, b being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & a : ( ( ) ( ) set ) <> b : ( ( ) ( ) set ) holds
not R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ;

theorem :: WELLORD1:48
for Z being ( ( ) ( ) set )
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & Z : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
( F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ) ;

theorem :: WELLORD1:49
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
ex b being ( ( ) ( ) set ) st
( b : ( ( ) ( ) set ) in field S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: WELLORD1:50
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_isomorphism_of R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) holds
for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) holds
ex b being ( ( ) ( ) set ) st
( b : ( ( ) ( ) set ) in field S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ) ;

theorem :: WELLORD1:51
for a, b, c being ( ( ) ( ) set )
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & S : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in field S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & c : ( ( ) ( ) set ) in field S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic & R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic holds
( S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg c : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg b : ( ( ) ( ) set ) : ( ( ) ( ) set ) & [c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in S : ( ( Relation-like ) ( Relation-like ) Relation) ) ;

theorem :: WELLORD1:52
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & S : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & not R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic & ( for a being ( ( ) ( ) set ) holds
( not a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) or not R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ) ) holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in field S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (S : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ) ;

theorem :: WELLORD1:53
for Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st Y : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering & not R : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic holds
ex a being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) in field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 (R : ( ( Relation-like ) ( Relation-like ) Relation) -Seg a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) ,R : ( ( Relation-like ) ( Relation-like ) Relation) |_2 Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic ) ;

theorem :: WELLORD1:54
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) are_isomorphic & R : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering holds
S : ( ( Relation-like ) ( Relation-like ) Relation) is well-ordering ;