TarskiEuclid2Space is (FS) by ThMak2;
then ( TarskiEuclid2Space is (RE) & TarskiEuclid2Space is (TE) & TarskiEuclid2Space is (FS') ) by ThMak3;
hence ex b₁ being (RE) (TE) (FS') TarskiGeometryStruct st b₁ is (SC) ; :: thesis: verum