let OAS be OAffinSpace; :: thesis: for o, a, b, a', b' being Element of the carrier of OAS st not LIN o,a,b & o,a // o,a' & LIN o,b,b' & a,b '||' a',b' holds
( o,b // o,b' & a,b // a',b' )
let o, a, b, a', b' be Element of OAS; :: thesis: ( not LIN o,a,b & o,a // o,a' & LIN o,b,b' & a,b '||' a',b' implies ( o,b // o,b' & a,b // a',b' ) )
assume that
A1:
not LIN o,a,b
and
A2:
o,a // o,a'
and
A3:
LIN o,b,b'
and
A4:
a,b '||' a',b'
; :: thesis: ( o,b // o,b' & a,b // a',b' )
consider a2 being Element of OAS such that
A5:
Mid a,o,a2
and
A6:
o <> a2
by DIRAF:17;
A7:
a,o // o,a2
by A5, DIRAF:def 3;
A8:
( o <> a & o <> b & b <> a )
by A1, DIRAF:37;
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;
LIN a,o,a2
by A5, DIRAF:34;
then A11:
LIN o,a2,a
by DIRAF:36;
Mid b,o,b2
by A9, DIRAF:def 3;
then
LIN b,o,b2
by DIRAF:34;
then A12:
LIN b2,o,b
by DIRAF:36;
A13:
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, A11, DIRAF:37, DIRAF:39;
hence
contradiction
by A1, A6, A11, DIRAF:38;
:: thesis: verum
end;
A14:
not LIN o,a2,b2
proof
assume A15:
LIN o,
a2,
b2
;
:: thesis: contradiction
LIN o,
a2,
o
by DIRAF:37;
then A16:
LIN b2,
o,
a
by A6, A11, A15, DIRAF:38;
LIN b2,
o,
o
by DIRAF:37;
hence
contradiction
by A1, A12, A13, A16, DIRAF:38;
:: thesis: verum
end;
then A17:
a2 <> b2
by DIRAF:37;
A18:
a2,o // o,a'
A19:
a2,b2 '||' a',b'
LIN o,b2,b'
proof
Mid b,
o,
b2
by A9, DIRAF:def 3;
then
LIN b,
o,
b2
by DIRAF:34;
then
(
LIN o,
b,
b2 &
LIN o,
b,
o )
by DIRAF:36, DIRAF:37;
hence
LIN o,
b2,
b'
by A3, A8, DIRAF:38;
:: thesis: verum
end;
then A20:
( a2,b2 // b',a' & b2,o // o,b' )
by A14, A18, A19, Th12;
o,b // b2,o
by A9, DIRAF:5;
hence
o,b // o,b'
by A13, A20, DIRAF:6; :: thesis: a,b // a',b'
( a,b // b2,a2 & b2,a2 // a',b' )
by A10, A20, DIRAF:5;
hence
a,b // a',b'
by A17, DIRAF:6; :: thesis: verum