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