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 be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [z,b₁] in (NOT O1) OR (NOT O2) or [z,b₁] in NOT (O1 AND O2) )
let s be set ; :: 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 Th4;
then ( z nin (dom O1) /\ (dom O2) & dom (O1 AND O2) c= (dom O1) /\ (dom O2) ) by RELAT_1:2, XBOOLE_0:def 4;
then z nin dom (O1 AND O2) ;
hence [z,s] in NOT (O1 AND O2) by A1, Th4; :: thesis: verum