let AFV be WeakAffVect; :: thesis: for a, b, c, p being Element of AFV holds
( Mid a,b,c iff Mid PSym p,a, PSym p,b, PSym p,c )
let a, b, c, p be Element of AFV; :: thesis: ( Mid a,b,c iff Mid PSym p,a, PSym p,b, PSym p,c )

A1: now

assume Mid PSym p,a, PSym p,b, PSym p,c ; :: thesis: Mid a,b,c
then PSym p,a, PSym p,b // PSym p,b, PSym p,c by Def3;
then a,b // b,c by Th40;
hence Mid a,b,c by Def3; :: thesis: verum

end;

now

assume Mid a,b,c ; :: thesis: Mid PSym p,a, PSym p,b, PSym p,c
then a,b // b,c by Def3;
then PSym p,a, PSym p,b // PSym p,b, PSym p,c by Th40;
hence Mid PSym p,a, PSym p,b, PSym p,c by Def3; :: thesis: verum

end;

hence ( Mid a,b,c iff Mid PSym p,a, PSym p,b, PSym p,c ) by A1; :: thesis: verum