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