let S be IncSpace; :: thesis: for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds
Line (A,B) = Line (A,C)
let A, B, C be POINT of S; :: thesis: ( A <> B & A <> C & {A,B,C} is linear implies Line (A,B) = Line (A,C) )
assume A1: A <> B ; :: thesis: ( not A <> C or not {A,B,C} is linear or Line (A,B) = Line (A,C) )
then A2: {A,B} on Line (A,B) by Def19;
then A3: A on Line (A,B) by Th1;
assume A4: A <> C ; :: thesis: ( not {A,B,C} is linear or Line (A,B) = Line (A,C) )
assume {A,B,C} is linear ; :: thesis: Line (A,B) = Line (A,C)
then C on Line (A,B) by A1, A2, Th18;
then {A,C} on Line (A,B) by A3, Th1;
hence Line (A,B) = Line (A,C) by A4, Def19; :: thesis: verum