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