theorem Th145: :: ABCMIZ_1:145

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