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 b1 being non empty (TE) (IE) (SC) TarskiGeometryStruct st b1 is (FS') ; :: thesis: verum