let A be Subset of L; :: thesis: ( A is lower implies A is Open )
assume A1: A is lower ; :: thesis: A is Open
let x be Element of L; :: according to WAYBEL_6:def 1 :: thesis: ( not x in A or ex b₁ being Element of the carrier of L st
( b₁ in A & b₁ is_way_below x ) )
assume A2: x in A ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in A & b₁ is_way_below x )
consider y being object such that
A3: y in waybelow x by XBOOLE_0:def 1;
reconsider y = y as Element of L by A3;
take y ; :: thesis: ( y in A & y is_way_below x )
y << x by A3, WAYBEL_3:7;
then y <= x by WAYBEL_3:1;
hence ( y in A & y is_way_below x ) by A1, A2, A3, WAYBEL_3:7; :: thesis: verum