let L be non empty antisymmetric RelStr ; :: thesis: ( ( L is with_suprema or L is with_infima ) implies for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed )
assume A1: ( L is with_suprema or L is with_infima ) ; :: thesis: for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed
let X, Y be Subset of L; :: thesis: ( X is lower & X is directed & Y is lower & Y is directed implies X /\ Y is directed )
assume that
A2: ( X is lower & X is directed ) and
A3: ( Y is lower & Y is directed ) ; :: thesis: X /\ Y is directed
A4: X /\ Y is lower by A2, A3, Th27;

per cases ( L is with_suprema or L is with_infima ) by A1;

suppose A5: L is with_suprema ; :: thesis: X /\ Y is directed

now

let x, y be Element of L; :: thesis: ( x in X /\ Y & y in X /\ Y implies x "\/" y in X /\ Y )
assume ( x in X /\ Y & y in X /\ Y ) ; :: thesis: x "\/" y in X /\ Y
then ( x in X & x in Y & y in X & y in Y ) by XBOOLE_0:def 4;
then ( x "\/" y in X & x "\/" y in Y ) by A2, A3, A5, Th40;
hence x "\/" y in X /\ Y by XBOOLE_0:def 4; :: thesis: verum

end;

hence X /\ Y is directed by A4, A5, Th40; :: thesis: verum

end;

suppose A6: L is with_infima ; :: thesis: X /\ Y is directed

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st
( z in X /\ Y & x <= z & y <= z ) )
assume ( x in X /\ Y & y in X /\ Y ) ; :: thesis: ex z being Element of L st
( z in X /\ Y & x <= z & y <= z )
then A7: ( x in X & x in Y & y in X & y in Y ) by XBOOLE_0:def 4;
then consider zx being Element of L such that
A8: ( zx in X & x <= zx & y <= zx ) by A2, Def1;
consider zy being Element of L such that
A9: ( zy in Y & x <= zy & y <= zy ) by A3, A7, Def1;
take z = zx "/\" zy; :: thesis: ( z in X /\ Y & x <= z & y <= z )
( z <= zx & z <= zy ) by A6, YELLOW_0:23;
then ( z in X & z in Y ) by A2, A3, A8, A9, Def19;
hence z in X /\ Y by XBOOLE_0:def 4; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A6, A8, A9, YELLOW_0:23; :: thesis: verum

end;

end;