let OAS be OAffinSpace; ( OAS is satisfying_DES_1 implies OAS is satisfying_DES )
assume A1:
OAS is satisfying_DES_1
; OAS is satisfying_DES
for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
proof
let o,
a,
b,
c,
a1,
b1,
c1 be
Element of
OAS;
( o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that A2:
o,
a // o,
a1
and A3:
o,
b // o,
b1
and A4:
o,
c // o,
c1
and A5:
not
o,
a,
b are_collinear
and A6:
not
o,
a,
c are_collinear
and A7:
a,
b // a1,
b1
and A8:
a,
c // a1,
c1
;
b,c // b1,c1
consider a2 being
Element of
OAS such that A9:
Mid a,
o,
a2
and A10:
o <> a2
by DIRAF:13;
A11:
a,
o // o,
a2
by A9, DIRAF:def 3;
A12:
o <> a
by A5, DIRAF:31;
then consider c2 being
Element of
OAS such that A13:
c,
o // o,
c2
and A14:
c,
a // a2,
c2
by A11, ANALOAF:def 5;
A15:
c2,
a2 // a,
c
by A14, DIRAF:2;
A16:
c2,
o // o,
c
by A13, DIRAF:2;
then
Mid c2,
o,
c
by DIRAF:def 3;
then A17:
c2,
o,
c are_collinear
by DIRAF:28;
a,
o,
a2 are_collinear
by A9, DIRAF:28;
then A18:
o,
a2,
a are_collinear
by DIRAF:30;
A19:
o <> c2
proof
assume
o = c2
;
contradiction
then
o,
a2 // a,
c
by A14, DIRAF:2;
then
o,
a2 '||' a,
c
by DIRAF:def 4;
then
(
o,
a2,
o are_collinear &
o,
a2,
c are_collinear )
by A10, A18, DIRAF:31, DIRAF:33;
hence
contradiction
by A6, A10, A18, DIRAF:32;
verum
end;
A20:
not
o,
a2,
c2 are_collinear
proof
A21:
c2,
o,
o are_collinear
by DIRAF:31;
A22:
o,
a2,
o are_collinear
by DIRAF:31;
assume
o,
a2,
c2 are_collinear
;
contradiction
then
c2,
o,
a are_collinear
by A10, A18, A22, DIRAF:32;
hence
contradiction
by A6, A17, A19, A21, DIRAF:32;
verum
end;
consider b2 being
Element of
OAS such that A23:
b,
o // o,
b2
and A24:
b,
a // a2,
b2
by A12, A11, ANALOAF:def 5;
A25:
b2,
a2 // a,
b
by A24, DIRAF:2;
a <> b
by A5, DIRAF:31;
then
b2,
a2 // a1,
b1
by A7, A25, DIRAF:3;
then A26:
a2,
b2 // b1,
a1
by DIRAF:2;
o <> c
by A6, DIRAF:31;
then A27:
c2,
o // o,
c1
by A4, A16, DIRAF:3;
A28:
a,
c // c2,
a2
by A14, ANALOAF:def 5;
A29:
b2,
o // o,
b
by A23, DIRAF:2;
then
Mid b2,
o,
b
by DIRAF:def 3;
then A30:
b2,
o,
b are_collinear
by DIRAF:28;
A31:
o <> b2
proof
assume
o = b2
;
contradiction
then
o,
a2 // a,
b
by A24, DIRAF:2;
then
o,
a2 '||' a,
b
by DIRAF:def 4;
then
(
o,
a2,
o are_collinear &
o,
a2,
b are_collinear )
by A10, A18, DIRAF:31, DIRAF:33;
hence
contradiction
by A5, A10, A18, DIRAF:32;
verum
end;
A32:
not
o,
a2,
b2 are_collinear
proof
A33:
b2,
o,
o are_collinear
by DIRAF:31;
A34:
o,
a2,
o are_collinear
by DIRAF:31;
assume
o,
a2,
b2 are_collinear
;
contradiction
then
b2,
o,
a are_collinear
by A10, A18, A34, DIRAF:32;
hence
contradiction
by A5, A30, A31, A33, DIRAF:32;
verum
end;
A35:
now ( c2 = b2 implies b,c // b1,c1 )
b2,
a2 // a,
b
by A24, DIRAF:2;
then A36:
b2,
a2 '||' a,
b
by DIRAF:def 4;
assume A37:
c2 = b2
;
b,c // b1,c1then A38:
o,
b2,
c are_collinear
by A17, DIRAF:30;
c2,
a2 // a,
c
by A14, DIRAF:2;
then A39:
b2,
a2 '||' a,
c
by A37, DIRAF:def 4;
( not
o,
b2,
a2 are_collinear &
o,
b2,
b are_collinear )
by A30, A32, DIRAF:30;
then
b = c
by A18, A38, A36, A39, PASCH:4;
hence
b,
c // b1,
c1
by DIRAF:4;
verum end;
a2,
o // o,
a
by A11, DIRAF:2;
then A40:
a2,
o // o,
a1
by A2, A12, DIRAF:3;
a <> c
by A6, DIRAF:31;
then
c2,
a2 // a1,
c1
by A8, A15, DIRAF:3;
then A41:
a2,
c2 // c1,
a1
by DIRAF:2;
o <> b
by A5, DIRAF:31;
then
b2,
o // o,
b1
by A3, A29, DIRAF:3;
then A42:
c2,
b2 // b1,
c1
by A1, A40, A27, A41, A26, A32, A20;
a,
b // b2,
a2
by A24, ANALOAF:def 5;
then
b,
c // c2,
b2
by A1, A5, A6, A11, A23, A13, A28;
hence
b,
c // b1,
c1
by A42, A35, DIRAF:3;
verum
end;
hence
OAS is satisfying_DES
; verum