let S be non empty (TE) (IE) (SC) (RE') TarskiGeometryStruct ; :: thesis: S is (RE)
let a, b be POINT of S; :: according to GTARSKI3:def 15 :: thesis: a,b equiv b,a

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: a,b equiv b,a

hence a,b equiv b,a by Satz2p8; :: thesis: verum

end;

suppose A1: a <> b ; :: thesis: a,b equiv b,a

( between b,a,a & S is (RE') ) by Satz3p1;
hence a,b equiv b,a by A1, Satz2p2bis; :: thesis: verum

end;

end;