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