let AFV be WeakAffVect; :: thesis: for a, b, c, p being Element of AFV ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)
let a, b, c, p be Element of AFV; :: thesis: ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)
consider e being Element of AFV such that
A1: Mid a,e,c by Th19;
consider d being Element of AFV such that
A2: Mid b,e,d by Th21;
c = PSym (e,a) by A1, Def4;
then PSym (c,(PSym (d,p))) = PSym ((PSym (e,a)),(PSym ((PSym (e,b)),p))) by A2, Def4
.= PSym ((PSym (e,a)),(PSym (e,(PSym (b,(PSym (e,p))))))) by Th37
.= PSym (e,(PSym (a,(PSym (e,(PSym (e,(PSym (b,(PSym (e,p))))))))))) by Th37
.= PSym (e,(PSym (a,(PSym (b,(PSym (e,p))))))) by Th29
.= PSym (e,(PSym (e,(PSym (b,(PSym (a,p))))))) by Th39
.= PSym (b,(PSym (a,p))) by Th29 ;
then PSym (d,p) = PSym (c,(PSym (b,(PSym (a,p))))) by Th29;
hence ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p) by Th39; :: thesis: verum