let X be TopSpace; :: thesis: for A being open Subset of (Omega X) holds A is upper
let A be open Subset of (Omega X); :: thesis: A is upper
let x, y be Element of (Omega X); :: according to WAYBEL_0:def 20 :: thesis: ( not x in A or not x <= y or y in A )
assume A1: x in A ; :: thesis: ( not x <= y or y in A )
assume x <= y ; :: thesis: y in A
then A2: ex Z being Subset of X st
( Z = {y} & x in Cl Z ) by Def2;
then reconsider X = X as non empty TopSpace ;
reconsider y = y as Element of (Omega X) ;
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then x in Cl {y} by A2, TOPS_3:80;
then A meets {y} by A1, PRE_TOPC:def 7;
hence y in A by ZFMISC_1:50; :: thesis: verum