let IPP be IncProjSp; :: thesis: for o, a, b, c being POINT of
for A, B, P, Q being LINE of 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 o, a, b, c be POINT of ; :: thesis: for A, B, P, Q being LINE of 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 ; :: thesis: ( 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 ) ; :: thesis: P <> Q
assume not P <> Q ; :: thesis: contradiction
then P = B by A2, A4, INCPROJ:def 9;
hence contradiction by A1, A3, INCPROJ:def 9; :: thesis: verum