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