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, s be object ; :: according to RELAT_1:def 2 :: 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 Th36;
then z nin (dom O1) \/ (dom O2) by XTUPLE_0:23;
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, Th36;
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 A2: ( z = s & z in X & z nin dom O1 & z nin dom O2 ) by Th36;
then z nin (dom O1) \/ (dom O2) by XBOOLE_0:def 3;
then z nin dom (O1 OR O2) by XTUPLE_0:23;
hence [z,s] in NOT (O1 OR O2) by A2, Th36; :: thesis: verum