let L be antisymmetric with_infima RelStr ; :: thesis: for X being upper Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
let X be upper Subset of L; :: thesis: ( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
thus ( X is filtered implies for x, y being Element of L st x in X & y in X holds
x "/\" y in X ) :: thesis: ( ( for x, y being Element of L st x in X & y in X holds
x "/\" y in X ) 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: for x, y being Element of L st x in X & y in X holds
x "/\" y in X
let x, y be Element of L; :: thesis: ( x in X & y in X implies x "/\" y in X )
assume ( x in X & y in X ) ; :: thesis: x "/\" y in X
then consider z being Element of L such that
A2: ( z in X & x >= z & y >= z ) by A1;
x "/\" y >= z by A2, YELLOW_0:23;
hence x "/\" y in X by A2, Def20; :: thesis: verum

end;

assume A3: for x, y being Element of L st x in X & y in X holds
x "/\" y in X ; :: 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 ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
then ( x "/\" y in X & x >= x "/\" y & y >= x "/\" y ) by A3, YELLOW_0:23;
hence ex z being Element of L st
( z in X & z <= x & z <= y ) ; :: thesis: verum