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 )
assume A1: ( a = b or a = c or b = c or a = d or b = d or d = c ) ; :: thesis: a,b,c,d are_coplanar

A2: now

assume ( a = b or a = c or b = c ) ; :: thesis: a,b,c,d are_coplanar
then a,b,c is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by Th10; :: thesis: verum

end;

A3: now

assume ( a = d or b = d ) ; :: thesis: a,b,c,d are_coplanar
then d,a,b is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by Th10; :: thesis: verum

end;

now

assume d = c ; :: thesis: a,b,c,d are_coplanar
then b,c,d is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by Th10; :: thesis: verum

end;

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