let AFV be WeakAffVect; for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
let a, b, c, d, p be Element of AFV; ( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
A1:
now ( PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) implies a,b // c,d )assume A2:
PSym (
p,
a),
PSym (
p,
b)
// PSym (
p,
c),
PSym (
p,
d)
;
a,b // c,d
d,
c // PSym (
p,
c),
PSym (
p,
d)
by Th32;
then
d,
c // PSym (
p,
a),
PSym (
p,
b)
by A2, Def1;
then A3:
c,
d // PSym (
p,
b),
PSym (
p,
a)
by Th7;
a,
b // PSym (
p,
b),
PSym (
p,
a)
by Th32;
hence
a,
b // c,
d
by A3, Def1;
verum end;
now ( a,b // c,d implies PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )A4:
PSym (
p,
b),
PSym (
p,
a)
// a,
b
by Th3, Th32;
assume A5:
a,
b // c,
d
;
PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d)
PSym (
p,
d),
PSym (
p,
c)
// c,
d
by Th3, Th32;
then
PSym (
p,
d),
PSym (
p,
c)
// a,
b
by A5, Def1;
then
PSym (
p,
b),
PSym (
p,
a)
// PSym (
p,
d),
PSym (
p,
c)
by A4, Def1;
hence
PSym (
p,
a),
PSym (
p,
b)
// PSym (
p,
c),
PSym (
p,
d)
by Th7;
verum end;
hence
( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
by A1; verum