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 A2: ( x in uparrow X & y in uparrow X ) ; :: thesis: ex z being Element of L st
( z in uparrow X & z <= x & z <= y )
then consider x' being Element of L such that
A3: ( x >= x' & x' in X ) by Def16;
consider y' being Element of L such that
A4: ( y >= y' & y' in X ) by A2, Def16;
consider z being Element of L such that
A5: ( z in X & x' >= z & y' >= z ) by A1, A3, A4;
take z ; :: thesis: ( z in uparrow X & z <= x & z <= y )
z >= z by ORDERS_2:24;
hence z in uparrow X by A5, Def16; :: thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A3, A4, A5, ORDERS_2:26; :: thesis: verum

end;

set Y = uparrow X;
assume A6: 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 A7: ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
( x >= x & y >= y ) by ORDERS_2:24;
then ( x in uparrow X & y in uparrow X ) by A7, Def16;
then consider z being Element of L such that
A8: ( z in uparrow X & x >= z & y >= z ) by A6;
consider z' being Element of L such that
A9: ( z >= z' & z' in X ) by A8, Def16;
take z' ; :: thesis: ( z' in X & z' <= x & z' <= y )
thus z' in X by A9; :: thesis: ( z' <= x & z' <= y )
thus ( z' <= x & z' <= y ) by A8, A9, ORDERS_2:26; :: thesis: verum