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