let R be Relation; :: thesis: for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y
let X, Y be set ; :: 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_transitive_in X by A1, WELLORD1:def 5;
A4: R is_connected_in X by A1, WELLORD1:def 5;
A5: R is_antisymmetric_in X by A1, WELLORD1:def 5;
A6: R is_well_founded_in X by A1, WELLORD1:def 5;
R is_reflexive_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, A5, A4, Lm10, Th93, Th94, Th95; :: 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
A7: Z c= Y and
A8: Z <> {} ; :: thesis: ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z )
Z c= X by A2, A7, XBOOLE_1:1;
hence ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z ) by A8, A6, WELLORD1:def 3; :: thesis: verum