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:
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 ; :: 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