let AFV be WeakAffVect; :: thesis: for o, a, b being Element of AFV holds
( Pcom o,a = b iff a,o // o,b )
let o, a, b be Element of AFV; :: thesis: ( Pcom o,a = b iff a,o // o,b )

A1: now

assume a,o // o,b ; :: thesis: Pcom o,a = b
then Mid a,o,b by Def3;
hence Pcom o,a = b by Def4; :: thesis: verum

end;

now

assume Pcom o,a = b ; :: thesis: a,o // o,b
then Mid a,o,b by Def4;
hence a,o // o,b by Def3; :: thesis: verum

end;

hence ( Pcom o,a = b iff a,o // o,b ) by A1; :: thesis: verum