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

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

hence
X \/ Y is well_founded Subset of R
; :: thesis: verum
let Z be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Z c= XY or Z = {} or ex b_{1} being object st

( b_{1} in Z & the InternalRel of R -Seg b_{1} misses Z ) )

assume that

A4: Z c= XY and

A5: Z <> {} ; :: thesis: ex b_{1} being object st

( b_{1} in Z & the InternalRel of R -Seg b_{1} misses Z )

set XZ = X /\ Z;

A6: X /\ Z c= X by XBOOLE_1:17;

end;( b

assume that

A4: Z c= XY and

A5: Z <> {} ; :: thesis: ex b

( b

set XZ = X /\ Z;

A6: X /\ Z c= X by XBOOLE_1:17;

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

end;

suppose
X /\ Z = {}
; :: thesis: ex b_{1} being object st

( b_{1} in Z & the InternalRel of R -Seg b_{1} misses Z )

( b

then
X misses Z
;

then Z c= Y by A4, XBOOLE_1:73;

hence ex b_{1} being object st

( b_{1} in Z & the InternalRel of R -Seg b_{1} misses Z )
by A2, A5; :: thesis: verum

end;then Z c= Y by A4, XBOOLE_1:73;

hence ex b

( b

suppose
X /\ Z <> {}
; :: thesis: ex b_{1} being object st

( b_{1} in Z & the InternalRel of R -Seg b_{1} misses Z )

( b

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;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