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