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 Th24;
consider d being Element of AFV such that
A2: Mid b,e,d by Th26;
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 Th44
.= PSym e,(PSym a,(PSym e,(PSym e,(PSym b,(PSym e,p))))) by Th44
.= PSym e,(PSym a,(PSym b,(PSym e,p))) by Th36
.= PSym e,(PSym e,(PSym b,(PSym a,p))) by Th46
.= PSym b,(PSym a,p) by Th36 ;
then PSym d,p = PSym c,(PSym b,(PSym a,p)) by Th36;
hence ex d being Element of AFV st PSym a,(PSym b,(PSym c,p)) = PSym d,p by Th46; :: thesis: verum