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 )
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;
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;
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 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;
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
hence a,b,c,d are_coplanar by A1, A2, A3; :: thesis: verum