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 b₁ being object st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z ) )
assume that
A4: Z c= XY and
A5: Z <> {} ; :: thesis: ex b₁ being object st
( b₁ in Z & the InternalRel of R -Seg b₁ 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 b₁ being object st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z )

then X misses Z ;
then Z c= Y by A4, XBOOLE_1:73;
hence ex b₁ being object st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z ) by A2, A5; :: thesis: verum

end;

suppose X /\ Z <> {} ; :: thesis: ex b₁ being object st
( b₁ in Z & the InternalRel of R -Seg b₁ 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 A7, XBOOLE_0:def 4;
take a ; :: thesis: ( a in Z & the InternalRel of R -Seg a misses Z )
thus a in Z by A7, XBOOLE_0:def 4; :: 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 A10, XBOOLE_0:def 4;
A12: b in the InternalRel of R -Seg a by A10, XBOOLE_0:def 4;
then [b,a] in the InternalRel of R by WELLORD1:1;
then b in X by A1, A9;
then b in X /\ Z by A11, XBOOLE_0:def 4;
hence contradiction by A8, A12, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence X \/ Y is well_founded Subset of R ; :: thesis: verum