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
( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_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, 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
A3: Z c= Y and
A4: Z <> {} ; :: thesis: ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z )
( Z c= X & R is_well_founded_in X ) by A1, A2, A3, WELLORD1:def 5, XBOOLE_1:1;
hence ex b₁ being set st
( b₁ in Z & R -Seg b₁ misses Z ) by A4, WELLORD1:def 3; :: thesis: verum