TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation ;
hence ex b₁ being TarskiGeometryStruct st
( b₁ is (RE) & b₁ is (TE) ) ; :: thesis: verum