set Y = the strict discrete TopStruct ;
take the strict discrete TopStruct ; :: thesis: ( the strict discrete TopStruct is almost_discrete & the strict discrete TopStruct is strict )
thus ( the strict discrete TopStruct is almost_discrete & the strict discrete TopStruct is strict ) ; :: thesis: verum