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 } )

( 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 A13:
X = union { (wayabove x) where x is Element of L : x in X }
; :: thesis: 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 }

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

proof

union { (wayabove x) where x is Element of L : x in X } c= X
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;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

proof

hence
X = union { (wayabove x) where x is Element of L : x in X }
by A2; :: thesis: verum
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;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

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 )

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