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