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 Th11;
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, Th39;
then {A,C} on Line A,B by A3, Th11;
hence Line A,B = Line A,C by A4, Def19; :: thesis: verum