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;