theorem :: ABCMIZ_1:146

for C being initialized ConstructorSignature
for f being valuation of C
for A, B being Subset of (QuasiAdjs C) st A c= B holds
A at f c= B at f