let PCPP be CollProjectiveSpace; :: thesis: for a, b, c, d being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds
a = d
let a, b, c, d be Element of PCPP; :: thesis: ( not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear implies a = d )
assume A1: ( not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear ) ; :: thesis: a = d
assume A2: not a = d ; :: thesis: contradiction
( a,d,a is_collinear & a,d,b is_collinear & a,d,c is_collinear ) by A1, Th3, ANPROJ_2:def 7;
hence contradiction by A1, A2, ANPROJ_2:def 8; :: thesis: verum