let AFV be WeakAffVect; for a, p, q being Element of AFV holds
( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
let a, p, q be Element of AFV; ( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
A1:
now ( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) implies ( ( p = q or MDist q,p or MDist q, PSym (p,q) ) & ( p = q or MDist p,q or MDist q, PSym (p,q) ) ) )assume
PSym (
p,
(PSym (q,a)))
= PSym (
q,
(PSym (p,a)))
;
( ( p = q or MDist q,p or MDist q, PSym (p,q) ) & ( p = q or MDist p,q or MDist q, PSym (p,q) ) )then
PSym (
p,
(PSym (q,(PSym (p,a)))))
= PSym (
q,
a)
by Th29;
then
PSym (
(PSym (p,q)),
a)
= PSym (
q,
a)
by Th37;
then
(
q = PSym (
p,
q) or
MDist q,
PSym (
p,
q) )
by Th36;
then A2:
(
Mid q,
p,
q or
MDist q,
PSym (
p,
q) )
by Def4;
hence
(
p = q or
MDist q,
p or
MDist q,
PSym (
p,
q) )
;
( p = q or MDist p,q or MDist q, PSym (p,q) )thus
(
p = q or
MDist p,
q or
MDist q,
PSym (
p,
q) )
by A2, Th18;
verum end;
now ( ( p = q or MDist p,q or MDist q, PSym (p,q) ) implies PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) )assume
(
p = q or
MDist p,
q or
MDist q,
PSym (
p,
q) )
;
PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a)))then
(
Mid q,
p,
q or
MDist q,
PSym (
p,
q) )
by Th18;
then
PSym (
(PSym (p,q)),
a)
= PSym (
q,
a)
by Def4, Th36;
then
PSym (
p,
(PSym (q,(PSym (p,a)))))
= PSym (
q,
a)
by Th37;
hence
PSym (
p,
(PSym (q,a)))
= PSym (
q,
(PSym (p,a)))
by Th29;
verum end;
hence
( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
by A1; verum