let T be complete continuous Scott TopLattice; :: thesis: for S being upper Subset of T holds
( S is open iff S is Open )
let S be upper Subset of T; :: thesis: ( S is open iff S is Open )
thus ( S is open implies S is Open ) :: thesis: ( S is Open implies S is open )
proof
assume A1: S is open ; :: thesis: S is Open
let x be Element of T; :: according to WAYBEL_6:def 1 :: thesis: ( not x in S or ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x ) )
assume x in S ; :: thesis: ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x )
then ex y being Element of T st
( y << x & y in S ) by A1, Th43;
hence ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x ) ; :: thesis: verum
end;
thus ( S is Open implies S is open ) by Th41; :: thesis: verum