let L be RelStr ; :: thesis: for X, Y being Subset of L st X is upper & Y is upper holds
( X /\ Y is upper & X \/ Y is upper )
let X, Y be Subset of L; :: thesis: ( X is upper & Y is upper implies ( X /\ Y is upper & X \/ Y is upper ) )
assume that
A1: for x, y being Element of L st x in X & y >= x holds
y in X and
A2: for x, y being Element of L st x in Y & y >= x holds
y in Y ; :: according to WAYBEL_0:def 20 :: thesis: ( X /\ Y is upper & X \/ Y is upper )

hereby :: according to WAYBEL_0:def 20 :: thesis: X \/ Y is upper

let x, y be Element of L; :: thesis: ( x in X /\ Y & y >= x implies y in X /\ Y )
assume A3: x in X /\ Y ; :: thesis: ( y >= x implies y in X /\ Y )
then A4: x in X by XBOOLE_0:def 4;
A5: x in Y by A3, XBOOLE_0:def 4;
assume A6: y >= x ; :: thesis: y in X /\ Y
then A7: y in X by A1, A4;
y in Y by A2, A5, A6;
hence y in X /\ Y by A7, XBOOLE_0:def 4; :: thesis: verum

end;

let x, y be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( x in X \/ Y & x <= y implies y in X \/ Y )
assume x in X \/ Y ; :: thesis: ( not x <= y or y in X \/ Y )
then A8: ( x in X or x in Y ) by XBOOLE_0:def 3;
assume y >= x ; :: thesis: y in X \/ Y
then ( y in X or y in Y ) by A1, A2, A8;
hence y in X \/ Y by XBOOLE_0:def 3; :: thesis: verum