consider T being non empty trivial strict TopSpace;
take T ; :: thesis: ( T is strict & T is trivial & not T is empty )
thus ( T is strict & T is trivial & not T is empty ) ; :: thesis: verum