let OAS be OAffinSpace; :: thesis: for a, b, c, d, p being Element of OAS st Mid p,b,c & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear holds
Mid p,a,d
let a, b, c, d, p be Element of OAS; :: thesis: ( Mid p,b,c & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear implies Mid p,a,d )
assume that
A1: Mid p,b,c and
A2: p,a,d are_collinear and
A3: a,b '||' c,d and
A4: not p,a,b are_collinear ; :: thesis: Mid p,a,d
A5: now :: thesis: ( b <> c implies Mid p,a,d )
d,a,p are_collinear by A2, DIRAF:30;
then d,a '||' d,p by DIRAF:def 5;
then A6: a,d '||' d,p by DIRAF:22;
assume A7: b <> c ; :: thesis: Mid p,a,d
A8: b <> a by A4, DIRAF:31;
A9: not d,b,a are_collinear
proof
assume d,b,a are_collinear ; :: thesis: contradiction
then A10: a,b,d are_collinear by DIRAF:30;
a,b '||' d,c by A3, DIRAF:22;
then a,b,c are_collinear by A8, A10, DIRAF:33;
then A11: b,c,a are_collinear by DIRAF:30;
p,b,c are_collinear by A1, DIRAF:28;
then A12: b,c,p are_collinear by DIRAF:30;
b,c,b are_collinear by DIRAF:31;
hence contradiction by A4, A7, A11, A12, DIRAF:32; :: thesis: verum
end;
then d <> a by DIRAF:31;
then consider q being Element of OAS such that
A13: b,d '||' d,q and
A14: b,a '||' p,q by A6, DIRAF:27;
A15: p,b,c are_collinear by A1, DIRAF:28;
A16: p <> c by A1, A7, DIRAF:8;
A17: not b,c,d are_collinear
proof
A18: p,c,c are_collinear by DIRAF:31;
p,b,c are_collinear by A1, DIRAF:28;
then A19: p,c,b are_collinear by DIRAF:30;
assume A20: b,c,d are_collinear ; :: thesis: contradiction
A21: b,c,b are_collinear by DIRAF:31;
c,d,b are_collinear by A20, DIRAF:30;
then c,d '||' c,b by DIRAF:def 5;
then p,a,c are_collinear by A2, A3, A22, DIRAF:23;
then p,c,a are_collinear by DIRAF:30;
then b,c,a are_collinear by A16, A19, A18, DIRAF:32;
hence contradiction by A7, A9, A20, A21, DIRAF:32; :: thesis: verum
end;
a,b '||' q,p by A14, DIRAF:22;
then A23: c,d '||' q,p by A3, A8, DIRAF:23;
d,b '||' d,q by A13, DIRAF:22;
then d,b,q are_collinear by DIRAF:def 5;
then A24: b,d,q are_collinear by DIRAF:30;
A25: d <> p
proof
A26: p,c,p are_collinear by DIRAF:31;
p,b,c are_collinear by A1, DIRAF:28;
then A27: p,c,b are_collinear by DIRAF:30;
assume d = p ; :: thesis: contradiction
then p,c '||' b,a by A3, DIRAF:22;
then p,c,a are_collinear by A16, A27, DIRAF:33;
hence contradiction by A4, A16, A27, A26, DIRAF:32; :: thesis: verum
end;
A28: not d,p,q are_collinear
proof
A32: p,q,p are_collinear by DIRAF:31;
A33: d,p,p are_collinear by DIRAF:31;
assume A34: d,p,q are_collinear ; :: thesis: contradiction
d,p,a are_collinear by A2, DIRAF:30;
then A35: p,q,a are_collinear by A25, A34, A33, DIRAF:32;
p,q '||' a,b by A14, DIRAF:22;
then p,q,b are_collinear by A35, A29, DIRAF:33;
hence contradiction by A4, A35, A29, A32, DIRAF:32; :: thesis: verum
end;
Mid c,b,p by A1, DIRAF:9;
then A36: Mid d,b,q by A17, A24, A23, Th6;
A37: now :: thesis: not Mid p,d,a
d,b '||' d,q by A13, DIRAF:22;
then d,b,q are_collinear by DIRAF:def 5;
then A38: d,q,b are_collinear by DIRAF:30;
assume A39: Mid p,d,a ; :: thesis: contradiction
p,q '||' b,a by A14, DIRAF:22;
then Mid q,d,b by A28, A39, A38, Th6;
then Mid b,d,q by DIRAF:9;
then b = d by A36, DIRAF:14;
hence contradiction by A9, DIRAF:31; :: thesis: verum
end;
assume not Mid p,a,d ; :: thesis: contradiction
then Mid a,p,d by A2, A37, DIRAF:29;
then Mid b,p,c by A3, A4, A15, Th6;
then p = b by A1, DIRAF:14;
hence contradiction by A4, DIRAF:31; :: thesis: verum
end;
now :: thesis: ( b = c implies Mid p,a,d )
A40: a,b '||' b,a by DIRAF:19;
A41: p,a,a are_collinear by DIRAF:31;
A42: p,b,b are_collinear by DIRAF:31;
assume b = c ; :: thesis: Mid p,a,d
then a = d by A2, A3, A4, A42, A41, A40, Th4;
hence Mid p,a,d by DIRAF:10; :: thesis: verum
end;
hence Mid p,a,d by A5; :: thesis: verum