let IPP be IncProjSp; :: thesis: 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; :: 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 & 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 & 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 4;
hence contradiction by A1, A3, INCPROJ:def 4; :: thesis: verum