theorem LineEqA1: :: GTARSKI1:41

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S st a <> b holds
a,b equal_line b,a