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
A2: the InternalRel of R is_well_founded_in X by Def3;
A3: the InternalRel of R is_well_founded_in Y by Def3;
reconsider XY = X \/ Y as Subset of R ;
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 set st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z ) )
assume A4: ( Z c= XY & Z <> {} ) ; :: thesis: ex b₁ being set st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z )
set XZ = X /\ Z;
A5: X /\ Z c= X by XBOOLE_1:17;

per cases ( X /\ Z = {} or X /\ Z <> {} ) ;

suppose X /\ Z = {} ; :: thesis: ex b₁ being set st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z )

then X misses Z by XBOOLE_0:def 7;
then Z c= Y by A4, XBOOLE_1:73;
hence ex b₁ being set st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z ) by A3, A4, WELLORD1:def 3; :: thesis: verum

end;

suppose X /\ Z <> {} ; :: thesis: ex b₁ being set st
( b₁ in Z & the InternalRel of R -Seg b₁ misses Z )

then consider a being set such that
A6: ( a in X /\ Z & the InternalRel of R -Seg a misses X /\ Z ) by A2, A5, WELLORD1:def 3;
take a ; :: thesis: ( a in Z & the InternalRel of R -Seg a misses Z )
thus a in Z by A6, 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 set such that
A7: b in (the InternalRel of R -Seg a) /\ Z by XBOOLE_0:def 1;
A8: ( b in the InternalRel of R -Seg a & b in Z ) by A7, XBOOLE_0:def 4;
then A9: ( b <> a & [b,a] in the InternalRel of R ) by WELLORD1:def 1;
a in X by A6, XBOOLE_0:def 4;
then b in X by A1, A9, Def1;
then b in X /\ Z by A8, XBOOLE_0:def 4;
hence contradiction by A6, A8, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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