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 upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered )
assume A1:
( L is with_suprema or L is with_infima )
; for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered
let X, Y be Subset of L; ( X is upper & X is filtered & Y is upper & Y is filtered implies X /\ Y is filtered )
assume that
A2:
( X is upper & X is filtered )
and
A3:
( Y is upper & Y is filtered )
; X /\ Y is filtered
A4:
X /\ Y is upper
by A2, A3, Th29;
per cases
( L is with_infima or L is with_suprema )
by A1;
suppose A5:
L is
with_infima
;
X /\ Y is filtered 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, Th41;
x "/\" y in Y
by A3, A5, A9, A11, Th41;
hence
x "/\" y in X /\ Y
by A12, XBOOLE_0:def 4;
verum end; hence
X /\ Y is
filtered
by A4, A5, Th41;
verum suppose A13:
L is
with_suprema
;
X /\ Y is filtered let x,
y be
Element of
L;
WAYBEL_0:def 2 ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st
( z in X /\ Y & z <= x & z <= y ) )assume that A14:
x in X /\ Y
and A15:
y in X /\ Y
;
ex z being Element of L st
( z in X /\ Y & z <= x & z <= y )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 & z <= x & z <= y )A26:
z >= zx
by A13, YELLOW_0:22;
A27:
z >= zy
by A13, YELLOW_0:22;
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;
( z <= x & z <= y )thus
(
z <= x &
z <= y )
by A13, A21, A22, A24, A25, YELLOW_0:22;
verum end;