let AFV be WeakAffVect; :: thesis: 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; :: thesis: ( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
A1: now :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence ( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) ) by A1; :: thesis: verum