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 )

waybelow x meets X ; :: thesis: X is Open

( 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 A4:
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

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

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 )

hence
X is Open
; :: thesis: verumex 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;( 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