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 A1: ( ( for y being Element of L st y in X holds
y >= x ) & ( 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; :: thesis: verum

end;

assume A2: ( ( for y being Element of L st y in X holds
y <= x ) & ( 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 A2; :: thesis: verum