let A be non empty Subset of GRZ-formula-set; :: thesis: for t, u being GRZ-formula st A, GRZ-rules |- t '&' u holds
A, GRZ-rules |- u '&' t
let t, u be GRZ-formula; :: thesis: ( A, GRZ-rules |- t '&' u implies A, GRZ-rules |- u '&' t )
assume A, GRZ-rules |- t '&' u ; :: thesis: A, GRZ-rules |- u '&' t
then ( A, GRZ-rules |- t & A, GRZ-rules |- u ) by Th60;
hence A, GRZ-rules |- u '&' t by Th60; :: thesis: verum