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

{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