let L be up-complete LATTICE; :: thesis: for X being upper Subset of L holds
( X is Open iff X = union { () where x is Element of L : x in X } )

let X be upper Subset of L; :: thesis: ( X is Open iff X = union { () where x is Element of L : x in X } )
hereby :: thesis: ( X = union { () where x is Element of L : x in X } implies X is Open )
assume A1: X is Open ; :: thesis: X = union { () where x is Element of L : x in X }
A2: X c= union { () where x is Element of L : x in X }
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in union { () where x is Element of L : x in X } )
assume A3: z in X ; :: thesis: z in union { () where x is Element of L : x in X }
then reconsider x1 = z as Element of X ;
reconsider x1 = x1 as Element of L by A3;
consider y being Element of L such that
A4: y in X and
A5: y << x1 by A1, A3;
x1 in { y1 where y1 is Element of L : y1 >> y } by A5;
then A6: x1 in wayabove y by WAYBEL_3:def 4;
wayabove y in { () where x is Element of L : x in X } by A4;
hence z in union { () where x is Element of L : x in X } by ; :: thesis: verum
end;
union { () where x is Element of L : x in X } c= X
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { () where x is Element of L : x in X } or z in X )
assume z in union { () where x is Element of L : x in X } ; :: thesis: z in X
then consider Y being set such that
A7: z in Y and
A8: Y in { () where x is Element of L : x in X } by TARSKI:def 4;
consider x being Element of L such that
A9: Y = wayabove x and
A10: x in X by A8;
z in { y where y is Element of L : y >> x } by ;
then consider z1 being Element of L such that
A11: z1 = z and
A12: z1 >> x ;
x <= z1 by ;
hence z in X by ; :: thesis: verum
end;
hence X = union { () where x is Element of L : x in X } by A2; :: thesis: verum
end;
assume A13: X = union { () where x is Element of L : x in X } ; :: thesis: X is Open
now :: thesis: for x1 being Element of L st x1 in X holds
ex x being Element of L st
( x in X & x << x1 )
let x1 be Element of L; :: thesis: ( x1 in X implies ex x being Element of L st
( x in X & x << x1 ) )

assume x1 in X ; :: thesis: ex x being Element of L st
( x in X & x << x1 )

then consider Y being set such that
A14: x1 in Y and
A15: Y in { () where x is Element of L : x in X } by ;
consider x being Element of L such that
A16: Y = wayabove x and
A17: x in X by A15;
x1 in { y where y is Element of L : y >> x } by ;
then ex z1 being Element of L st
( z1 = x1 & z1 >> x ) ;
hence ex x being Element of L st
( x in X & x << x1 ) by A17; :: thesis: verum
end;
hence X is Open ; :: thesis: verum