let L be RelStr ; :: thesis: for X, Y being set
for x being Element of L holds
( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) )
let X, Y be set ; :: thesis: for x being Element of L holds
( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) )
let x be Element of L; :: thesis: ( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) )
thus ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) :: thesis: ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y )

proof

assume that
A1: for y being Element of L st y in X holds
y >= x and
A2: for y being Element of L st y in Y holds
y >= x ; :: according to LATTICE3:def 8 :: thesis: x is_<=_than X \/ Y
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in X \/ Y or x <= y )
( not y in X \/ Y or y in X or y in Y ) by XBOOLE_0:def 3;
hence ( not y in X \/ Y or x <= y ) by A1, A2; :: thesis: verum

end;

assume that
A3: for y being Element of L st y in X holds
y <= x and
A4: for y being Element of L st y in Y holds
y <= x ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than X \/ Y
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in X \/ Y or y <= x )
( not y in X \/ Y or y in X or y in Y ) by XBOOLE_0:def 3;
hence ( not y in X \/ Y or y <= x ) by A3, A4; :: thesis: verum