let L be with_infima Poset; :: thesis: for X being Subset of L st X is Open & X is lower holds

X is filtered

let X be Subset of L; :: thesis: ( X is Open & X is lower implies X is filtered )

assume A1: ( X is Open & X is lower ) ; :: thesis: X is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in X or not y in X or ex b_{1} being Element of the carrier of L st

( b_{1} in X & b_{1} <= x & b_{1} <= y ) )

assume that

A2: x in X and

y in X ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in X & b_{1} <= x & b_{1} <= y )

A3: x "/\" y <= x by YELLOW_0:23;

then x "/\" y in X by A1, A2;

then consider z being Element of L such that

A4: z in X and

A5: z << x "/\" y by A1;

take z ; :: thesis: ( z in X & z <= x & z <= y )

( x "/\" y <= y & z <= x "/\" y ) by A5, WAYBEL_3:1, YELLOW_0:23;

hence ( z in X & z <= x & z <= y ) by A3, A4, ORDERS_2:3; :: thesis: verum

X is filtered

let X be Subset of L; :: thesis: ( X is Open & X is lower implies X is filtered )

assume A1: ( X is Open & X is lower ) ; :: thesis: X is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in X or not y in X or ex b

( b

assume that

A2: x in X and

y in X ; :: thesis: ex b

( b

A3: x "/\" y <= x by YELLOW_0:23;

then x "/\" y in X by A1, A2;

then consider z being Element of L such that

A4: z in X and

A5: z << x "/\" y by A1;

take z ; :: thesis: ( z in X & z <= x & z <= y )

( x "/\" y <= y & z <= x "/\" y ) by A5, WAYBEL_3:1, YELLOW_0:23;

hence ( z in X & z <= x & z <= y ) by A3, A4, ORDERS_2:3; :: thesis: verum