let AFV be WeakAffSegm; :: thesis: for a, b, p, p', c being Element of st a,b // p,p' & a,b // b,c & a,p // p,b & a,p' // p',b holds
a = c
let a, b, p, p', c be Element of ; :: thesis: ( a,b // p,p' & a,b // b,c & a,p // p,b & a,p' // p',b implies a = c )
assume that
A1: a,b // p,p' and
A2: a,b // b,c and
A3: a,p // p,b and
A4: a,p' // p',b ; :: thesis: a = c
p,b // a,p by A3, Th2;
then p,b // p,a by Th3;
then A5: b,p // p,a by Th4;
p',b // a,p' by A4, Th2;
then p',b // p',a by Th3;
then A6: b,p' // p',a by Th4;
b,a // p,p' by A1, Th4;
then a,a // a,c by A2, A5, A6, Def2;
then a,c // a,a by Th2;
hence a = c by Def2; :: thesis: verum