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;

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;

end;

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

end;

now :: thesis: for x, y being Element of L st x in X /\ Y & y in X /\ Y holds

x "\/" y in X /\ Y

hence
X /\ Y is directed
by A4, A5, Th40; :: thesis: verumx "\/" y in X /\ Y

let x, y be Element of L; :: thesis: ( x in X /\ Y & y in X /\ Y implies x "\/" y in X /\ Y )

assume that

A6: x in X /\ Y and

A7: y in X /\ Y ; :: thesis: x "\/" y in X /\ Y

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: verum

end;assume that

A6: x in X /\ Y and

A7: y in X /\ Y ; :: thesis: x "\/" y in X /\ Y

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: verum

suppose A13:
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 that

A14: x in X /\ Y and

A15: y in X /\ Y ; :: thesis: ex z being Element of L st

( z in X /\ Y & x <= z & y <= z )

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: ( z in X /\ Y & x <= z & y <= z )

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: ( x <= z & y <= z )

thus ( x <= z & y <= z ) by A13, A21, A22, A24, A25, YELLOW_0:23; :: thesis: verum

end;( z in X /\ Y & x <= z & y <= z ) )

assume that

A14: x in X /\ Y and

A15: y in X /\ Y ; :: thesis: ex z being Element of L st

( z in X /\ Y & x <= z & y <= z )

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: ( z in X /\ Y & x <= z & y <= z )

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: ( x <= z & y <= z )

thus ( x <= z & y <= z ) by A13, A21, A22, A24, A25, YELLOW_0:23; :: thesis: verum