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