consider Y being strict discrete TopStruct ;
take Y ; :: thesis: ( Y is almost_discrete & Y is strict )
thus ( Y is almost_discrete & Y is strict ) ; :: thesis: verum