( TarskiEuclid2Space is (FS) & TarskiEuclid2Space is (Co) ) by GTARSKI2:def 2, ThMak2;
hence ex b₁ being non empty TarskiGeometryStruct st
( b₁ is (RE) & b₁ is (TE) & b₁ is (IE) & b₁ is (SC) & b₁ is (FS) & b₁ is (IB) & b₁ is (Pa) & b₁ is (Lo2) & b₁ is (Up2) & b₁ is (Eu) & b₁ is (Co) ) by GTARSKI2:def 2; :: thesis: verum