let S be IncSpace; :: thesis: for A being POINT of S

for L being LINE of S ex B being POINT of S st

( A <> B & B on L )

let A be POINT of S; :: thesis: for L being LINE of S ex B being POINT of S st

( A <> B & B on L )

let L be LINE of S; :: thesis: ex B being POINT of S st

( A <> B & B on L )

consider B, C being POINT of S such that

A1: B <> C and

A2: {B,C} on L by Def8;

A3: ( A <> C or A <> B ) by A1;

( B on L & C on L ) by A2, Th1;

hence ex B being POINT of S st

( A <> B & B on L ) by A3; :: thesis: verum

for L being LINE of S ex B being POINT of S st

( A <> B & B on L )

let A be POINT of S; :: thesis: for L being LINE of S ex B being POINT of S st

( A <> B & B on L )

let L be LINE of S; :: thesis: ex B being POINT of S st

( A <> B & B on L )

consider B, C being POINT of S such that

A1: B <> C and

A2: {B,C} on L by Def8;

A3: ( A <> C or A <> B ) by A1;

( B on L & C on L ) by A2, Th1;

hence ex B being POINT of S st

( A <> B & B on L ) by A3; :: thesis: verum