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 )

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: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 ; :: thesis: ( z9 in X & z9 <= x & z9 <= y )

thus z9 in X by A21; :: thesis: ( z9 <= x & z9 <= y )

thus ( z9 <= x & z9 <= y ) by A18, A19, A20, ORDERS_2:3; :: thesis: verum

( 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

set Y = uparrow X;
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 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 ; :: thesis: ( z in uparrow X & z <= x & z <= y )

z >= z by ORDERS_2:1;

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:3; :: thesis: verum

end;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 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 ; :: thesis: ( z in uparrow X & z <= x & z <= y )

z >= z by ORDERS_2:1;

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:3; :: thesis: verum

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: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 ; :: thesis: ( z9 in X & z9 <= x & z9 <= y )

thus z9 in X by A21; :: thesis: ( z9 <= x & z9 <= y )

thus ( z9 <= x & z9 <= y ) by A18, A19, A20, ORDERS_2:3; :: thesis: verum