TrivialTarskiSpace is (IE) ;
hence ex b₁ being non empty (IE) (SC) TarskiGeometryStruct st b₁ is trivial ; :: thesis: verum