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

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