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

hereby :: thesis: ( X = union { (wayabove x) where x is Element of L : x in X } implies X is Open )

assume A1: X is Open ; :: thesis: X = union { (wayabove x) where x is Element of L : x in X }
A2: X c= union { (wayabove x) where x is Element of L : x in X }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in union { (wayabove x) where x is Element of L : x in X } )
assume A3: z in X ; :: thesis: z in union { (wayabove x) 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 & y << x1 ) by A1, A3, Def1;
x1 in { y1 where y1 is Element of L : y1 >> y } by A4;
then A5: x1 in wayabove y by WAYBEL_3:def 4;
wayabove y in { (wayabove x) where x is Element of L : x in X } by A4;
hence z in union { (wayabove x) where x is Element of L : x in X } by A5, TARSKI:def 4; :: thesis: verum

end;

union { (wayabove x) where x is Element of L : x in X } c= X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (wayabove x) where x is Element of L : x in X } or z in X )
assume z in union { (wayabove x) where x is Element of L : x in X } ; :: thesis: z in X
then consider Y being set such that
A6: z in Y and
A7: Y in { (wayabove x) where x is Element of L : x in X } by TARSKI:def 4;
consider x being Element of L such that
A8: ( Y = wayabove x & x in X ) by A7;
z in { y where y is Element of L : y >> x } by A6, A8, WAYBEL_3:def 4;
then consider z1 being Element of L such that
A9: ( z1 = z & z1 >> x ) ;
x <= z1 by A9, WAYBEL_3:1;
hence z in X by A8, A9, WAYBEL_0:def 20; :: thesis: verum

end;

hence X = union { (wayabove x) where x is Element of L : x in X } by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume A10: X = union { (wayabove x) where x is Element of L : x in X } ; :: thesis: X is Open

now

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
A11: x1 in Y and
A12: Y in { (wayabove x) where x is Element of L : x in X } by A10, TARSKI:def 4;
consider x being Element of L such that
A13: ( Y = wayabove x & x in X ) by A12;
x1 in { y where y is Element of L : y >> x } by A11, A13, WAYBEL_3:def 4;
then consider z1 being Element of L such that
A14: ( z1 = x1 & z1 >> x ) ;
thus ex x being Element of L st
( x in X & x << x1 ) by A13, A14; :: thesis: verum

end;

hence X is Open by Def1; :: thesis: verum