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