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 object ; :: 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 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 { (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 A6, TARSKI:def 4; :: thesis: verum

end;

union { (wayabove x) 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 { (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
A7: z in Y and
A8: 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
A9: Y = wayabove x and
A10: x in X by A8;
z in { y where y is Element of L : y >> x } by A7, A9, WAYBEL_3:def 4;
then consider z1 being Element of L such that
A11: z1 = z and
A12: z1 >> x ;
x <= z1 by A12, WAYBEL_3:1;
hence z in X by A10, A11, WAYBEL_0:def 20; :: thesis: verum

end;

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

end;

assume A13: X = union { (wayabove x) 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 { (wayabove x) where x is Element of L : x in X } by A13, TARSKI:def 4;
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 A14, A16, WAYBEL_3:def 4;
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