let X, Y be set ; :: thesis: for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
let R be Relation; :: thesis: ( R well_orders X & Y c= X implies R well_orders Y )
assume that
A1: R well_orders X and
A2: Y c= X ; :: thesis: R well_orders Y
A3: ( R is_antisymmetric_in X & R is_connected_in X ) by A1, WELLORD1:def 5;
A4: R is_well_founded_in X by A1, WELLORD1:def 5;
( R is_reflexive_in X & R is_transitive_in X ) by A1, WELLORD1:def 5;
hence ( R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y & R is_connected_in Y ) by A2, A3, Lm4, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def 5 :: thesis: R is_well_founded_in Y
let Z be set ; :: according to WELLORD1:def 3 :: thesis: ( not Z c= Y or Z = {} or ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z ) )
assume that
A5: Z c= Y and
A6: Z <> {} ; :: thesis: ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z )
Z c= X by A2, A5, XBOOLE_1:1;
hence ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z ) by A6, A4, WELLORD1:def 3; :: thesis: verum