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_{1} being Element of the carrier of L st

( b_{1} in A & b_{1} is_way_below x ) )

assume A2: x in A ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in A & b_{1} 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

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

( b

assume A2: x in A ; :: thesis: ex b

( b

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