let AFV be WeakAffVect; :: thesis: for a, p, q being Element of AFV holds
( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )
let a, p, q be Element of AFV; :: thesis: ( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )
A1: now :: thesis: ( MDist p,q implies PSym (p,a) = PSym (q,a) )
assume A2: MDist p,q ; :: thesis: PSym (p,a) = PSym (q,a)
( Mid a,p, PSym (p,a) & Mid a,q, PSym (q,a) ) by Def4;
hence PSym (p,a) = PSym (q,a) by A2, Th24; :: thesis: verum
end;
now :: thesis: ( not PSym (p,a) = PSym (q,a) or p = q or MDist p,q )
assume A3: PSym (p,a) = PSym (q,a) ; :: thesis: ( p = q or MDist p,q )
( Mid a,p, PSym (p,a) & Mid a,q, PSym (q,a) ) by Def4;
hence ( p = q or MDist p,q ) by A3, Th20; :: thesis: verum
end;
hence ( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) ) by A1; :: thesis: verum