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

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