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

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