theorem Th57: :: ABCMIZ_1:57

for C being initialized ConstructorSignature
for e being expression of C st e . {} = [non_op, the carrier of C] holds
ex a being expression of C, an_Adj C st e = (non_op C) term a