let T be 1 -element reflexive TopRelStr ; :: thesis: ( T is TopSpace-like implies T is Scott )
assume T is TopSpace-like ; :: thesis: T is Scott
then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ;
W is Scott

proof

let S be Subset of W; :: according to WAYBEL11:def 5 :: thesis: ( ( not S is open or S is upper ) & ( not S is upper or S is open ) )
thus ( S is open implies S is upper ) ; :: thesis: ( not S is upper or S is open )
thus ( not S is upper or S is open ) by TDLAT_3:15; :: thesis: verum

end;

hence T is Scott ; :: thesis: verum