let IPP be IncProjSp; for a, b, c, o being POINT of IPP
for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q
let a, b, c, o be POINT of IPP; for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q
let A, B, P, Q be LINE of IPP; ( o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q implies P <> Q )
assume that
A1:
( o on A & o on B & A <> B & a on A & o <> a )
and
A2:
( b on B & c on B & b <> c )
and
A3:
a on P
and
A4:
( b on P & c on Q )
; P <> Q
assume
not P <> Q
; contradiction
then
P = B
by A2, A4, INCPROJ:def 4;
hence
contradiction
by A1, A3, INCPROJ:def 4; verum