let X be set ; :: thesis: for O1, O2 being Operation of X holds (NOT O1) OR (NOT O2) c= NOT (O1 AND O2)
let O1, O2 be Operation of X; :: thesis: (NOT O1) OR (NOT O2) c= NOT (O1 AND O2)
let z, s be object ; :: according to RELAT_1:def 3 :: thesis: ( not [z,s] in (NOT O1) OR (NOT O2) or [z,s] in NOT (O1 AND O2) )
assume [z,s] in (NOT O1) OR (NOT O2) ; :: thesis: [z,s] in NOT (O1 AND O2)
then ( [z,s] in NOT O1 or [z,s] in NOT O2 ) by XBOOLE_0:def 3;
then A1: ( s = z & z in X & ( z nin dom O1 or z nin dom O2 ) ) by Th36;
then ( z nin (dom O1) /\ (dom O2) & dom (O1 AND O2) c= (dom O1) /\ (dom O2) ) by XBOOLE_0:def 4, XTUPLE_0:24;
then z nin dom (O1 AND O2) ;
hence [z,s] in NOT (O1 AND O2) by A1, Th36; :: thesis: verum