theorem CongruenceDoubleSymmetry: :: GTARSKI1:25

for S being satisfying_Tarski-model TarskiPlane
for a, b, c, d being POINT of S st a,b equiv c,d holds
b,a equiv d,c