now :: thesis: ( TrivialTarskiSpace is (RE) & TrivialTarskiSpace is (TE) & TrivialTarskiSpace is (FS') & not TrivialTarskiSpace is empty )

TrivialTarskiSpace is (FS) by ThMak2;
hence ( TrivialTarskiSpace is (RE) & TrivialTarskiSpace is (TE) & TrivialTarskiSpace is (FS') ) by ThMak3; :: thesis: not TrivialTarskiSpace is empty
thus not TrivialTarskiSpace is empty ; :: thesis: verum

end;

hence ex b₁ being non empty (TE) (IE) (SC) TarskiGeometryStruct st b₁ is (RE') ; :: thesis: verum