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 that
A1: not a,b,c is_collinear and
A2: ( a,b,d is_collinear & a,c,d is_collinear ) ; :: thesis: a = d
assume A3: not a = d ; :: thesis: contradiction
A4: a,d,a is_collinear by ANPROJ_2:def 7;
( a,d,b is_collinear & a,d,c is_collinear ) by A2, Th3;
hence contradiction by A1, A3, A4, ANPROJ_2:def 8; :: thesis: verum