consider T being non empty trivial finite discrete reflexive strict TopRelStr ;
take T ; :: thesis: ( T is trivial & T is complete & T is strict & not T is empty & T is Scott )
thus ( T is trivial & T is complete & T is strict & not T is empty ) ; :: thesis: T is Scott
let S be Subset of T; :: according to WAYBEL11:def 5 :: thesis: ( S is open iff S is upper )
thus ( S is open iff S is upper ) by TDLAT_3:17; :: thesis: verum