'not' in GRZ-ops by ENUMSET1:def 1;
hence GRZ-arity . 'not' = GRZ-op-arity . 'not' by Lm10
.= 1 by Def3 ;
:: thesis: ( GRZ-arity . '&' = 2 & GRZ-arity . '=' = 2 )
'&' in GRZ-ops by ENUMSET1:def 1;
hence GRZ-arity . '&' = GRZ-op-arity . '&' by Lm10
.= 2 by Def3 ;
:: thesis: GRZ-arity . '=' = 2
'=' in GRZ-ops by ENUMSET1:def 1;
hence GRZ-arity . '=' = GRZ-op-arity . '=' by Lm10
.= 2 by Def3 ;
:: thesis: verum