let AFV be WeakAffVect; for a, a', b, b', p being Element of st a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' holds
a,b '||' a',b'
let a, a', b, b', p be Element of ; ( a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' implies a,b '||' a',b' )
assume that
A1:
a <> a'
and
A2:
b <> b'
and
A3:
p,a '||' p,a'
and
A4:
p,b '||' p,b'
; a,b '||' a',b'
b,p // p,b'
by A2, A4, Lm1, Lm3;
then A5:
Mid b,p,b'
by AFVECT0:def 3;
a,p // p,a'
by A1, A3, Lm1, Lm3;
then
Mid a,p,a'
by AFVECT0:def 3;
then
a,b // b',a'
by A5, AFVECT0:30;
hence
a,b '||' a',b'
by DIRAF:def 4; verum