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