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 )

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

( 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; :: according to WAYBEL_0:def 20 :: thesis: ( x in X \/ Y & x <= y implies y in X \/ Y )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;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

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