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₁ being Element of the carrier of L st
( b₁ in X & b₁ <= x & b₁ <= y ) )
assume A2: ( x in X & y in X ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in X & b₁ <= x & b₁ <= y )
A3: ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
then x "/\" y in X by A1, A2, WAYBEL_0:def 19;
then consider z being Element of L such that
A4: z in X and
A5: z << x "/\" y by A1, WAYBEL_6:def 1;
take z ; :: thesis: ( z in X & z <= x & z <= y )
z <= x "/\" y by A5, WAYBEL_3:1;
hence ( z in X & z <= x & z <= y ) by A3, A4, ORDERS_2:26; :: thesis: verum