let L be complete Scott TopLattice; :: thesis: for X being Subset of L holds
( X in sigma L iff X is open )
let X be Subset of L; :: thesis: ( X in sigma L iff X is open )
sigma L = the topology of L by Th23;
hence ( X in sigma L iff X is open ) by PRE_TOPC:def 2; :: thesis: verum