set T = the non empty trivial finite discrete reflexive strict TopRelStr ;
take the non empty trivial finite discrete reflexive strict TopRelStr ; :: thesis: ( the non empty trivial finite discrete reflexive strict TopRelStr is trivial & the non empty trivial finite discrete reflexive strict TopRelStr is complete & the non empty trivial finite discrete reflexive strict TopRelStr is strict & not the non empty trivial finite discrete reflexive strict TopRelStr is empty & the non empty trivial finite discrete reflexive strict TopRelStr is Scott )
thus ( the non empty trivial finite discrete reflexive strict TopRelStr is trivial & the non empty trivial finite discrete reflexive strict TopRelStr is complete & the non empty trivial finite discrete reflexive strict TopRelStr is strict & not the non empty trivial finite discrete reflexive strict TopRelStr is empty ) ; :: thesis: the non empty trivial finite discrete reflexive strict TopRelStr is Scott
let S be Subset of the non empty trivial finite discrete reflexive strict TopRelStr ; :: 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