let L be non empty reflexive transitive RelStr ; for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
let X be Subset of L; ( X is filtered iff uparrow X is filtered )
thus
( X is filtered implies uparrow X is filtered )
( uparrow X is filtered implies X is filtered )proof
assume A1:
for
x,
y being
Element of
L st
x in X &
y in X holds
ex
z being
Element of
L st
(
z in X &
x >= z &
y >= z )
;
WAYBEL_0:def 2 uparrow X is filtered
let x,
y be
Element of
L;
WAYBEL_0:def 2 ( x in uparrow X & y in uparrow X implies ex z being Element of L st
( z in uparrow X & z <= x & z <= y ) )
assume that A2:
x in uparrow X
and A3:
y in uparrow X
;
ex z being Element of L st
( z in uparrow X & z <= x & z <= y )
consider x9 being
Element of
L such that A4:
x >= x9
and A5:
x9 in X
by A2, Def16;
consider y9 being
Element of
L such that A6:
y >= y9
and A7:
y9 in X
by A3, Def16;
consider z being
Element of
L such that A8:
z in X
and A9:
x9 >= z
and A10:
y9 >= z
by A1, A5, A7;
take
z
;
( z in uparrow X & z <= x & z <= y )
z >= z
by ORDERS_2:1;
hence
z in uparrow X
by A8, Def16;
( z <= x & z <= y )
thus
(
z <= x &
z <= y )
by A4, A6, A9, A10, ORDERS_2:3;
verum
end;
set Y = uparrow X;
assume A11:
for x, y being Element of L st x in uparrow X & y in uparrow X holds
ex z being Element of L st
( z in uparrow X & x >= z & y >= z )
; WAYBEL_0:def 2 X is filtered
let x, y be Element of L; WAYBEL_0:def 2 ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A12:
x in X
and
A13:
y in X
; ex z being Element of L st
( z in X & z <= x & z <= y )
A14:
x >= x
by ORDERS_2:1;
A15:
y >= y
by ORDERS_2:1;
A16:
x in uparrow X
by A12, A14, Def16;
y in uparrow X
by A13, A15, Def16;
then consider z being Element of L such that
A17:
z in uparrow X
and
A18:
x >= z
and
A19:
y >= z
by A11, A16;
consider z9 being Element of L such that
A20:
z >= z9
and
A21:
z9 in X
by A17, Def16;
take
z9
; ( z9 in X & z9 <= x & z9 <= y )
thus
z9 in X
by A21; ( z9 <= x & z9 <= y )
thus
( z9 <= x & z9 <= y )
by A18, A19, A20, ORDERS_2:3; verum