let S be non empty trivial (IE) (SC) TarskiGeometryStruct ; :: thesis: S is (RE)
let a, b be POINT of S; :: according to GTARSKI3:def 15 :: thesis: a,b equiv b,a
a = b by ZFMISC_1:def 10;
hence a,b equiv b,a by Satz2p8; :: thesis: verum