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 )

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 that

A8: x in X and

A9: y in X ; :: thesis: ex z being Element of L st

( z in X & z <= x & z <= y )

A10: x >= x "/\" y by YELLOW_0:23;

y >= x "/\" y by YELLOW_0:23;

hence ex z being Element of L st

( z in X & z <= x & z <= y ) by A7, A8, A9, A10; :: thesis: verum

( 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 A7:
for x, y being Element of L st x in X & y in X holds
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 that

A2: x in X and

A3: y in X ; :: thesis: x "/\" y in X

consider z being Element of L such that

A4: z in X and

A5: x >= z and

A6: y >= z by A1, A2, A3;

x "/\" y >= z by A5, A6, YELLOW_0:23;

hence x "/\" y in X by A4, Def20; :: thesis: verum

end;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 that

A2: x in X and

A3: y in X ; :: thesis: x "/\" y in X

consider z being Element of L such that

A4: z in X and

A5: x >= z and

A6: y >= z by A1, A2, A3;

x "/\" y >= z by A5, A6, YELLOW_0:23;

hence x "/\" y in X by A4, Def20; :: thesis: verum

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 that

A8: x in X and

A9: y in X ; :: thesis: ex z being Element of L st

( z in X & z <= x & z <= y )

A10: x >= x "/\" y by YELLOW_0:23;

y >= x "/\" y by YELLOW_0:23;

hence ex z being Element of L st

( z in X & z <= x & z <= y ) by A7, A8, A9, A10; :: thesis: verum