let AFV be WeakAffSegm; :: thesis: for a, b, c, p, p9 being Element of AFV st a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b holds
a = c
let a, b, c, p, p9 be Element of AFV; :: thesis: ( a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b implies a = c )
assume that
A1: a,b // p,p9 and
A2: a,b // b,c and
A3: a,p // p,b and
A4: a,p9 // p9,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;
p9,b // a,p9 by A4, Th2;
then p9,b // p9,a by Th3;
then A6: b,p9 // p9,a by Th4;
b,a // p,p9 by A1, Th4;
then a,a // a,c by A2, A5, A6, Def1;
then a,c // a,a by Th2;
hence a = c by Def1; :: thesis: verum