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

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