let L be RelStr ; :: thesis: for X, Y being Subset of L st X is lower & Y is lower holds

( X /\ Y is lower & X \/ Y is lower )

let X, Y be Subset of L; :: thesis: ( X is lower & Y is lower implies ( X /\ Y is lower & X \/ Y is lower ) )

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 19 :: thesis: ( X /\ Y is lower & X \/ Y is lower )

assume x in X \/ Y ; :: thesis: ( not y <= x 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 lower & X \/ Y is lower )

let X, Y be Subset of L; :: thesis: ( X is lower & Y is lower implies ( X /\ Y is lower & X \/ Y is lower ) )

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 19 :: thesis: ( X /\ Y is lower & X \/ Y is lower )

hereby :: according to WAYBEL_0:def 19 :: thesis: X \/ Y is lower

let x, y be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( x in X \/ Y & y <= x 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 y <= x 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