let PCPP be CollProjectiveSpace; :: thesis: for a1, a2, b1, b2, x, y being Element of PCPP st a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear holds
x = y
let a1, a2, b1, b2, x, y be Element of PCPP; :: thesis: ( a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear implies x = y )
assume A1: ( a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear ) ; :: thesis: x = y
assume A2: not x = y ; :: thesis: contradiction
A3: ( a1,a2,a1 is_collinear & a1,a2,a2 is_collinear & b1,b2,b1 is_collinear ) by ANPROJ_2:def 7;
then A4: x,y,b1 is_collinear by A1, ANPROJ_2:def 8;
A5: x,y,a1 is_collinear by A1, A3, ANPROJ_2:def 8;
x,y,a2 is_collinear by A1, A3, ANPROJ_2:def 8;
hence contradiction by A1, A2, A4, A5, ANPROJ_2:def 8; :: thesis: verum