let S be IncSpace; for A, B being POINT of S st A <> B holds
Line (A,B) = Line (B,A)
let A, B be POINT of S; ( A <> B implies Line (A,B) = Line (B,A) )
assume A1:
A <> B
; 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; verum