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 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 )
; :: thesis: 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; :: thesis: ( 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 )
; :: thesis: 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 A6:
L is
with_suprema
;
:: thesis: X /\ Y is filtered let x,
y be
Element of
L;
:: according to WAYBEL_0:def 2 :: thesis: ( 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
(
x in X /\ Y &
y in X /\ Y )
;
:: thesis: ex z being Element of L st
( z in X /\ Y & z <= x & z <= y )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, Def2;
consider zy being
Element of
L such that A9:
(
zy in Y &
x >= zy &
y >= zy )
by A3, A7, Def2;
take z =
zx "\/" zy;
:: thesis: ( z in X /\ Y & z <= x & z <= y )
(
z >= zx &
z >= zy )
by A6, YELLOW_0:22;
then
(
z in X &
z in Y )
by A2, A3, A8, A9, Def20;
hence
z in X /\ Y
by XBOOLE_0:def 4;
:: thesis: ( z <= x & z <= y )thus
(
z <= x &
z <= y )
by A6, A8, A9, YELLOW_0:22;
:: thesis: verum end;