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

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

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

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

then A36: Mid d,b,q by A17, A24, A23, Th6;

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;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

then
d <> a
by DIRAF:31;
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 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

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

a,b '||' q,p
by A14, DIRAF:22;
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;

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;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;

A22: now :: thesis: not a,b '||' c,b

c,d,b are_collinear
by A20, DIRAF:30;assume
a,b '||' c,b
; :: thesis: contradiction

then b,c '||' b,a by DIRAF:22;

then b,c,a are_collinear by DIRAF:def 5;

hence contradiction by A7, A9, A20, A21, DIRAF:32; :: thesis: verum

end;then b,c '||' b,a by DIRAF:22;

then b,c,a are_collinear by DIRAF:def 5;

hence contradiction by A7, A9, A20, A21, DIRAF:32; :: thesis: verum

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

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

A28:
not d,p,q are_collinear
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;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

proof

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;A29: now :: thesis: not p = q

A32:
p,q,p are_collinear
by DIRAF:31;assume
p = q
; :: thesis: contradiction

then d,b '||' d,p by A13, DIRAF:22;

then d,b,p are_collinear by DIRAF:def 5;

then A30: d,p,b are_collinear by DIRAF:30;

A31: d,p,d are_collinear by DIRAF:31;

d,p,a are_collinear by A2, DIRAF:30;

hence contradiction by A9, A25, A31, A30, DIRAF:32; :: thesis: verum

end;then d,b '||' d,p by A13, DIRAF:22;

then d,b,p are_collinear by DIRAF:def 5;

then A30: d,p,b are_collinear by DIRAF:30;

A31: d,p,d are_collinear by DIRAF:31;

d,p,a are_collinear by A2, DIRAF:30;

hence contradiction by A9, A25, A31, A30, DIRAF:32; :: thesis: verum

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

then A36: Mid d,b,q by A17, A24, A23, Th6;

A37: now :: thesis: not Mid p,d,a

assume
not Mid p,a,d
; :: thesis: contradiction
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;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

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

now :: thesis: ( b = c implies Mid p,a,d )

hence
Mid p,a,d
by A5; :: thesis: verumA40:
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;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