let AFV be WeakAffVect; :: thesis: for a, p, b being Element of ex c being Element of st PSym a,(PSym c,p) = PSym c,(PSym b,p)
let a, p, b be Element of ; :: thesis: ex c being Element of st PSym a,(PSym c,p) = PSym c,(PSym b,p)
consider c being Element of such that
A1: Mid a,c,b by Th24;
PSym b,p = PSym (PSym c,a),p by A1, Def4
.= PSym c,(PSym a,(PSym c,p)) by Th44 ;
then PSym c,(PSym b,p) = PSym a,(PSym c,p) by Th36;
hence ex c being Element of st PSym a,(PSym c,p) = PSym c,(PSym b,p) ; :: thesis: verum