let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d being Element of FCPS st not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear holds

a = d

let a, b, c, d be Element of FCPS; :: thesis: ( not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear implies a = d )

assume that

A1: not a,b,c are_collinear and

A2: ( a,b,d are_collinear & a,c,d are_collinear ) ; :: thesis: a = d

assume A3: not a = d ; :: thesis: contradiction

A4: a,d,a are_collinear by ANPROJ_2:def 7;

( a,d,b are_collinear & a,d,c are_collinear ) by A2, Th1;

hence contradiction by A1, A3, A4, ANPROJ_2:def 8; :: thesis: verum

a = d

let a, b, c, d be Element of FCPS; :: thesis: ( not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear implies a = d )

assume that

A1: not a,b,c are_collinear and

A2: ( a,b,d are_collinear & a,c,d are_collinear ) ; :: thesis: a = d

assume A3: not a = d ; :: thesis: contradiction

A4: a,d,a are_collinear by ANPROJ_2:def 7;

( a,d,b are_collinear & a,d,c are_collinear ) by A2, Th1;

hence contradiction by A1, A3, A4, ANPROJ_2:def 8; :: thesis: verum