let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
let X be Subset of L; :: thesis: ( X is filtered iff uparrow X is filtered )
thus
( X is filtered implies uparrow X is filtered )
:: thesis: ( 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 )
;
:: according to WAYBEL_0:def 2 :: thesis: uparrow X is filtered
let x,
y be
Element of
L;
:: according to WAYBEL_0:def 2 :: thesis: ( 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
;
:: thesis: ex z being Element of L st
( z in uparrow X & z <= x & z <= y )
consider x' being
Element of
L such that A4:
x >= x'
and A5:
x' in X
by A2, Def16;
consider y' being
Element of
L such that A6:
y >= y'
and A7:
y' in X
by A3, Def16;
consider z being
Element of
L such that A8:
z in X
and A9:
x' >= z
and A10:
y' >= z
by A1, A5, A7;
take
z
;
:: thesis: ( z in uparrow X & z <= x & z <= y )
z >= z
by ORDERS_2:24;
hence
z in uparrow X
by A8, Def16;
:: thesis: ( z <= x & z <= y )
thus
(
z <= x &
z <= y )
by A4, A6, A9, A10, ORDERS_2:26;
:: thesis: 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 )
; :: according to WAYBEL_0:def 2 :: thesis: X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( 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
; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
A14:
x >= x
by ORDERS_2:24;
A15:
y >= y
by ORDERS_2:24;
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 z' being Element of L such that
A20:
z >= z'
and
A21:
z' in X
by A17, Def16;
take
z'
; :: thesis: ( z' in X & z' <= x & z' <= y )
thus
z' in X
by A21; :: thesis: ( z' <= x & z' <= y )
thus
( z' <= x & z' <= y )
by A18, A19, A20, ORDERS_2:26; :: thesis: verum