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