let OAS be OAffinSpace; for p, a, b, a', b' being Element of st not LIN p,a,b & a,p // p,a' & b,p // p,b' & a,b '||' a',b' holds
a,b // b',a'
let p, a, b, a', b' be Element of ; ( not LIN p,a,b & a,p // p,a' & b,p // p,b' & a,b '||' a',b' implies a,b // b',a' )
assume that
A1:
not LIN p,a,b
and
A2:
a,p // p,a'
and
A3:
b,p // p,b'
and
A4:
a,b '||' a',b'
; a,b // b',a'
A5:
not LIN p,b,a
by A1, DIRAF:36;
Mid b,p,b'
by A3, DIRAF:def 3;
then
LIN b,p,b'
by DIRAF:34;
then A6:
LIN p,b,b'
by DIRAF:36;
Mid a,p,a'
by A2, DIRAF:def 3;
then
LIN a,p,a'
by DIRAF:34;
then A7:
LIN p,a,a'
by DIRAF:36;
A8:
b,a '||' a',b'
by A4, DIRAF:27;
a <> p
by A1, DIRAF:37;
then consider q being Element of such that
A9:
b,p // p,q
and
A10:
b,a // a',q
by A2, ANALOAF:def 5;
Mid b,p,q
by A9, DIRAF:def 3;
then
LIN b,p,q
by DIRAF:34;
then A11:
LIN p,b,q
by DIRAF:36;
b,a '||' a',q
by A10, DIRAF:def 4;
then
b,a // a',b'
by A10, A5, A7, A6, A11, A8, Th11;
hence
a,b // b',a'
by DIRAF:5; verum