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