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

per cases by A1;

suppose A5: L is with_suprema ; :: thesis:

let x, y be Element of L; :: thesis:
assume that
A6: x in X /\ Y and
A7: y in X /\ Y ; :: thesis:
A8: x in X by A6, XBOOLE_0:def 4;
A9: x in Y by A6, XBOOLE_0:def 4;
A10: y in X by A7, XBOOLE_0:def 4;
A11: y in Y by A7, XBOOLE_0:def 4;
A12: x "\/" y in X by A2, A5, A8, A10, Th40;
x "\/" y in Y by A3, A5, A9, A11, Th40;
hence x "\/" y in X /\ Y by A12, XBOOLE_0:def 4; :: thesis:

end;

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

end;

suppose A13: L is with_infima ; :: thesis:

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis:
assume that
A14: x in X /\ Y and
A15: y in X /\ Y ; :: thesis:
A16: x in X by A14, XBOOLE_0:def 4;
A17: x in Y by A14, XBOOLE_0:def 4;
A18: y in X by A15, XBOOLE_0:def 4;
A19: y in Y by A15, XBOOLE_0:def 4;
consider zx being Element of L such that
A20: zx in X and
A21: x <= zx and
A22: y <= zx by A2, A16, A18;
consider zy being Element of L such that
A23: zy in Y and
A24: x <= zy and
A25: y <= zy by A3, A17, A19;
take z = zx "/\" zy; :: thesis:
A26: z <= zx by A13, YELLOW_0:23;
A27: z <= zy by A13, YELLOW_0:23;
A28: z in X by A2, A20, A26;
z in Y by A3, A23, A27;
hence z in X /\ Y by A28, XBOOLE_0:def 4; :: thesis:
thus ( x <= z & y <= z ) by A13, A21, A22, A24, A25, YELLOW_0:23; :: thesis:

end;

end;