let T be non empty reflexive TopRelStr ; :: thesis: ( T is trivial & T is TopSpace-like implies T is Scott )
assume ( T is trivial & T is TopSpace-like ) ; :: thesis: T is Scott
then reconsider W = T as non empty trivial 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:17; :: thesis: verum

end;

hence T is Scott ; :: thesis: verum