let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d being Element of FCPS st ( a = b or a = c or b = c or a = d or b = d or d = c ) holds

a,b,c,d are_coplanar

let a, b, c, d be Element of FCPS; :: thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

hence a,b,c,d are_coplanar by A1, A2, A3; :: thesis: verum

a,b,c,d are_coplanar

let a, b, c, d be Element of FCPS; :: thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

A1: now :: thesis: ( ( a = b or a = c or b = c ) & ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

assume
( a = b or a = c or b = c )
; :: thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

then a,b,c are_collinear by ANPROJ_2:def 7;

hence ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; :: thesis: verum

end;then a,b,c are_collinear by ANPROJ_2:def 7;

hence ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; :: thesis: verum

A2: now :: thesis: ( ( a = d or b = d ) & ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

assume
( a = d or b = d )
; :: thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

then d,a,b are_collinear by ANPROJ_2:def 7;

hence ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; :: thesis: verum

end;then d,a,b are_collinear by ANPROJ_2:def 7;

hence ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; :: thesis: verum

A3: now :: thesis: ( d = c & ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

assume
( a = b or a = c or b = c or a = d or b = d or d = c )
; :: thesis: a,b,c,d are_coplanar assume
d = c
; :: thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )

then b,c,d are_collinear by ANPROJ_2:def 7;

hence ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; :: thesis: verum

end;then b,c,d are_collinear by ANPROJ_2:def 7;

hence ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; :: thesis: verum

hence a,b,c,d are_coplanar by A1, A2, A3; :: thesis: verum