let A be non empty Subset of GRZ-formula-set; :: thesis: for t, u being GRZ-formula st GRZ-axioms c= A & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u '=' t
let t, u be GRZ-formula; :: thesis: ( GRZ-axioms c= A & A, GRZ-rules |- t '=' u implies A, GRZ-rules |- u '=' t )
assume that
A1: GRZ-axioms c= A and
A2: A, GRZ-rules |- t '=' u ; :: thesis: A, GRZ-rules |- u '=' t
set v = (t '=' u) '=' (u '=' t);
(t '=' u) '=' (u '=' t) in GRZ-axioms by Def10;
then A, GRZ-rules |- (t '=' u) '=' (u '=' t) by A1, Th46;
hence A, GRZ-rules |- u '=' t by A2, Th61; :: thesis: verum