let OAS be OAffinSpace; :: thesis: ( OAS is satisfying_DES_1 implies OAS is satisfying_DES )
assume A1:
OAS is satisfying_DES_1
; :: thesis: 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 LIN o,a,b & not LIN o,a,c & 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;
:: thesis: ( o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that A2:
(
o,
a // o,
a1 &
o,
b // o,
b1 &
o,
c // o,
c1 )
and A3:
( not
LIN o,
a,
b & not
LIN o,
a,
c )
and A4:
(
a,
b // a1,
b1 &
a,
c // a1,
c1 )
;
:: thesis: b,c // b1,c1
consider a2 being
Element of
OAS such that A5:
Mid a,
o,
a2
and A6:
o <> a2
by DIRAF:17;
A7:
(
o <> a &
o <> b &
o <> c &
a <> b &
a <> c )
by A3, DIRAF:37;
A8:
a,
o // o,
a2
by A5, DIRAF:def 3;
then consider b2 being
Element of
OAS such that A9:
b,
o // o,
b2
and A10:
b,
a // a2,
b2
by A7, ANALOAF:def 5;
consider c2 being
Element of
OAS such that A11:
c,
o // o,
c2
and A12:
c,
a // a2,
c2
by A7, A8, ANALOAF:def 5;
(
a,
b // b2,
a2 &
a,
c // c2,
a2 )
by A10, A12, ANALOAF:def 5;
then A13:
b,
c // c2,
b2
by A1, A3, A8, A9, A11, Def16;
A14:
(
a2,
o // o,
a &
b2,
o // o,
b &
c2,
o // o,
c )
by A8, A9, A11, DIRAF:5;
then A15:
(
a2,
o // o,
a1 &
b2,
o // o,
b1 &
c2,
o // o,
c1 )
by A2, A7, DIRAF:6;
(
b2,
a2 // a,
b &
c2,
a2 // a,
c )
by A10, A12, DIRAF:5;
then
(
b2,
a2 // a1,
b1 &
c2,
a2 // a1,
c1 )
by A4, A7, DIRAF:6;
then A16:
(
a2,
c2 // c1,
a1 &
a2,
b2 // b1,
a1 )
by DIRAF:5;
LIN a,
o,
a2
by A5, DIRAF:34;
then A17:
LIN o,
a2,
a
by DIRAF:36;
(
Mid b2,
o,
b &
Mid c2,
o,
c )
by A14, DIRAF:def 3;
then A18:
(
LIN b2,
o,
b &
LIN c2,
o,
c )
by DIRAF:34;
A19:
o <> b2
proof
assume
o = b2
;
:: thesis: contradiction
then
o,
a2 // a,
b
by A10, DIRAF:5;
then
o,
a2 '||' a,
b
by DIRAF:def 4;
then
(
LIN o,
a2,
o &
LIN o,
a2,
b )
by A6, A17, DIRAF:37, DIRAF:39;
hence
contradiction
by A3, A6, A17, DIRAF:38;
:: thesis: verum
end;
A20:
not
LIN o,
a2,
b2
proof
assume A21:
LIN o,
a2,
b2
;
:: thesis: contradiction
LIN o,
a2,
o
by DIRAF:37;
then A22:
LIN b2,
o,
a
by A6, A17, A21, DIRAF:38;
LIN b2,
o,
o
by DIRAF:37;
hence
contradiction
by A3, A18, A19, A22, DIRAF:38;
:: thesis: verum
end;
A23:
o <> c2
proof
assume
o = c2
;
:: thesis: contradiction
then
o,
a2 // a,
c
by A12, DIRAF:5;
then
o,
a2 '||' a,
c
by DIRAF:def 4;
then
(
LIN o,
a2,
o &
LIN o,
a2,
c )
by A6, A17, DIRAF:37, DIRAF:39;
hence
contradiction
by A3, A6, A17, DIRAF:38;
:: thesis: verum
end;
not
LIN o,
a2,
c2
proof
assume A24:
LIN o,
a2,
c2
;
:: thesis: contradiction
LIN o,
a2,
o
by DIRAF:37;
then A25:
LIN c2,
o,
a
by A6, A17, A24, DIRAF:38;
LIN c2,
o,
o
by DIRAF:37;
hence
contradiction
by A3, A18, A23, A25, DIRAF:38;
:: thesis: verum
end;
then A26:
c2,
b2 // b1,
c1
by A1, A15, A16, A20, Def16;
now assume A27:
c2 = b2
;
:: thesis: b,c // b1,c1A28:
not
LIN o,
b2,
a2
by A20, DIRAF:36;
A29:
(
LIN o,
b2,
b &
LIN o,
b2,
c )
by A18, A27, DIRAF:36;
(
b2,
a2 // a,
b &
c2,
a2 // a,
c )
by A10, A12, DIRAF:5;
then
(
b2,
a2 '||' a,
b &
b2,
a2 '||' a,
c )
by A27, DIRAF:def 4;
then
b = c
by A17, A28, A29, PASCH:11;
hence
b,
c // b1,
c1
by DIRAF:7;
:: thesis: verum end;
hence
b,
c // b1,
c1
by A13, A26, DIRAF:6;
:: thesis: verum
end;
hence
OAS is satisfying_DES
by Def15; :: thesis: verum