let R be RelStr ; :: thesis: for X, Y being well_founded Subset of R st X is lower holds
X \/ Y is well_founded Subset of R

let X, Y be well_founded Subset of R; :: thesis: ( X is lower implies X \/ Y is well_founded Subset of R )
set r = the InternalRel of R;
assume A1: X is lower ; :: thesis: X \/ Y is well_founded Subset of R
reconsider XY = X \/ Y as Subset of R ;
A2: the InternalRel of R is_well_founded_in Y by Def3;
A3: the InternalRel of R is_well_founded_in X by Def3;
XY is well_founded
proof
let Z be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Z c= XY or Z = {} or ex b1 being object st
( b1 in Z & the InternalRel of R -Seg b1 misses Z ) )

assume that
A4: Z c= XY and
A5: Z <> {} ; :: thesis: ex b1 being object st
( b1 in Z & the InternalRel of R -Seg b1 misses Z )

set XZ = X /\ Z;
A6: X /\ Z c= X by XBOOLE_1:17;
per cases ( X /\ Z = {} or X /\ Z <> {} ) ;
suppose X /\ Z = {} ; :: thesis: ex b1 being object st
( b1 in Z & the InternalRel of R -Seg b1 misses Z )

then X misses Z ;
then Z c= Y by ;
hence ex b1 being object st
( b1 in Z & the InternalRel of R -Seg b1 misses Z ) by A2, A5; :: thesis: verum
end;
suppose X /\ Z <> {} ; :: thesis: ex b1 being object st
( b1 in Z & the InternalRel of R -Seg b1 misses Z )

then consider a being object such that
A7: a in X /\ Z and
A8: the InternalRel of R -Seg a misses X /\ Z by A3, A6;
A9: a in X by ;
take a ; :: thesis: ( a in Z & the InternalRel of R -Seg a misses Z )
thus a in Z by ; :: thesis: the InternalRel of R -Seg a misses Z
assume ( the InternalRel of R -Seg a) /\ Z <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider b being object such that
A10: b in ( the InternalRel of R -Seg a) /\ Z by XBOOLE_0:def 1;
A11: b in Z by ;
A12: b in the InternalRel of R -Seg a by ;
then [b,a] in the InternalRel of R by WELLORD1:1;
then b in X by A1, A9;
then b in X /\ Z by ;
hence contradiction by A8, A12, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
hence X \/ Y is well_founded Subset of R ; :: thesis: verum