let X be set ; :: thesis: for O1, O2 being Operation of X holds NOT (O1 OR O2) = (NOT O1) AND (NOT O2)
let O1, O2 be Operation of X; :: thesis: NOT (O1 OR O2) = (NOT O1) AND (NOT O2)
let z be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [z,b₁] in NOT (O1 OR O2) or [z,b₁] in (NOT O1) AND (NOT O2) ) & ( not [z,b₁] in (NOT O1) AND (NOT O2) or [z,b₁] in NOT (O1 OR O2) ) )
let s be set ; :: thesis: ( ( not [z,s] in NOT (O1 OR O2) or [z,s] in (NOT O1) AND (NOT O2) ) & ( not [z,s] in (NOT O1) AND (NOT O2) or [z,s] in NOT (O1 OR O2) ) )
thus ( [z,s] in NOT (O1 OR O2) implies [z,s] in (NOT O1) AND (NOT O2) ) :: thesis: ( not [z,s] in (NOT O1) AND (NOT O2) or [z,s] in NOT (O1 OR O2) )

proof

assume [z,s] in NOT (O1 OR O2) ; :: thesis: [z,s] in (NOT O1) AND (NOT O2)
then A1: ( z = s & z in X & z nin dom (O1 OR O2) ) by Th4;
then z nin (dom O1) \/ (dom O2) by RELAT_1:1;
then ( z nin dom O1 & z nin dom O2 ) by XBOOLE_0:def 3;
then ( [z,s] in NOT O1 & [z,s] in NOT O2 ) by A1, Th4;
hence [z,s] in (NOT O1) AND (NOT O2) by XBOOLE_0:def 4; :: thesis: verum

end;

assume [z,s] in (NOT O1) AND (NOT O2) ; :: thesis: [z,s] in NOT (O1 OR O2)
then ( [z,s] in NOT O1 & [z,s] in NOT O2 ) by XBOOLE_0:def 4;
then A1: ( z = s & z in X & z nin dom O1 & z nin dom O2 ) by Th4;
then z nin (dom O1) \/ (dom O2) by XBOOLE_0:def 3;
then z nin dom (O1 OR O2) by RELAT_1:1;
hence [z,s] in NOT (O1 OR O2) by A1, Th4; :: thesis: verum