let S be IncSpace; :: thesis: for A, B, C being POINT of S
for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear
let A, B, C be POINT of S; :: thesis: for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear
let L be LINE of S; :: thesis: ( A <> B & {A,B} on L & not C on L implies not {A,B,C} is linear )
assume that
A1: ( A <> B & {A,B} on L ) and
A2: not C on L ; :: thesis: not {A,B,C} is linear
given K being LINE of S such that A3: {A,B,C} on K ; :: according to INCSP_1:def 6 :: thesis: contradiction
{A,B} \/ {C} on K by A3, ENUMSET1:3;
then {A,B} on K by Th10;
then L = K by A1, Def10;
hence contradiction by A2, A3, Th2; :: thesis: verum