let L be non empty antisymmetric RelStr ; ( ( 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 )
; 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; ( 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 )
; 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
;
X /\ Y is directed now for x, y being Element of L st x in X /\ Y & y in X /\ Y holds
x "\/" y in X /\ Ylet x,
y be
Element of
L;
( 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
;
x "\/" y in X /\ YA8:
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;
verum end; hence
X /\ Y is
directed
by A4, A5, Th40;
verum suppose A13:
L is
with_infima
;
X /\ Y is directed let x,
y be
Element of
L;
WAYBEL_0:def 1 ( 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
;
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;
( 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;
( x <= z & y <= z )thus
(
x <= z &
y <= z )
by A13, A21, A22, A24, A25, YELLOW_0:23;
verum end;