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 Th11;
assume C on Line A,B ; :: thesis: {A,B,C} is linear
then {A,B,C} on Line A,B by A1, Th12;
hence {A,B,C} is linear by Def6; :: thesis: verum