let L be up-complete LATTICE; :: thesis: for X being upper Subset of L holds
( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )
let X be upper Subset of L; :: thesis: ( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )

hereby :: thesis: ( ( for x being Element of L st x in X holds
waybelow x meets X ) implies X is Open )

assume A1: X is Open ; :: thesis: for x being Element of L st x in X holds
waybelow x meets X
thus for x being Element of L st x in X holds
waybelow x meets X :: thesis: verum

proof

let x be Element of L; :: thesis: ( x in X implies waybelow x meets X )
assume x in X ; :: thesis: waybelow x meets X
then consider y being Element of L such that
A2: y in X and
A3: y << x by A1;
y in { y1 where y1 is Element of L : y1 << x } by A3;
then y in waybelow x by WAYBEL_3:def 3;
hence waybelow x meets X by A2, XBOOLE_0:3; :: thesis: verum

end;

end;

assume A4: for x being Element of L st x in X holds
waybelow x meets X ; :: thesis: X is Open

now :: thesis: for x1 being Element of L st x1 in X holds
ex z being Element of L st
( z in X & z << x1 )

let x1 be Element of L; :: thesis: ( x1 in X implies ex z being Element of L st
( z in X & z << x1 ) )
assume x1 in X ; :: thesis: ex z being Element of L st
( z in X & z << x1 )
then waybelow x1 meets X by A4;
then consider y being object such that
A5: y in waybelow x1 and
A6: y in X by XBOOLE_0:3;
waybelow x1 = { y1 where y1 is Element of L : y1 << x1 } by WAYBEL_3:def 3;
then ex z being Element of L st
( z = y & z << x1 ) by A5;
hence ex z being Element of L st
( z in X & z << x1 ) by A6; :: thesis: verum

end;

hence X is Open ; :: thesis: verum