let AFV be WeakAffVect; :: thesis: for a, b, c, p being Element of ex d being Element of st PSym a,(PSym b,(PSym c,p)) = PSym d,p
let a, b, c, p be Element of ; :: thesis: ex d being Element of st PSym a,(PSym b,(PSym c,p)) = PSym d,p
consider e being Element of such that
A1: Mid a,e,c by Th24;
consider d being Element of 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 st PSym a,(PSym b,(PSym c,p)) = PSym d,p by Th46; :: thesis: verum