consider A being non empty trivial TopSpace-like reflexive TopRelStr ;
take A ; :: thesis: ( A is reflexive & A is trivial & not A is empty & A is TopSpace-like )
thus ( A is reflexive & A is trivial & not A is empty & A is TopSpace-like ) ; :: thesis: verum