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