take (x. 1) '=' ((x. 1) '&' (x. 1)) ; :: thesis: ( (x. 1) '=' ((x. 1) '&' (x. 1)) is GRZ-axiomatic & (x. 1) '=' ((x. 1) '&' (x. 1)) is GRZ-provable & (x. 1) '=' ((x. 1) '&' (x. 1)) is LD-axiomatic & (x. 1) '=' ((x. 1) '&' (x. 1)) is LD-provable )
thus ( (x. 1) '=' ((x. 1) '&' (x. 1)) is GRZ-axiomatic & (x. 1) '=' ((x. 1) '&' (x. 1)) is GRZ-provable & (x. 1) '=' ((x. 1) '&' (x. 1)) is LD-axiomatic & (x. 1) '=' ((x. 1) '&' (x. 1)) is LD-provable ) ; :: thesis: verum