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) )

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

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) AND (NOT O2)
; :: thesis: [z,s] in NOT (O1 OR O2)
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;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

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