let S be IncSpace; :: thesis: for A, B being POINT of S st A <> B holds
Line A,B = Line B,A
let A, B be POINT of S; :: thesis: ( A <> B implies Line A,B = Line B,A )
assume A1: A <> B ; :: thesis: Line A,B = Line B,A
then {A,B} on Line A,B by Def19;
hence Line A,B = Line B,A by A1, Def19; :: thesis: verum