let X be set ; for O being Operation of X holds NOT O = id (X \ (dom O))
let O be Operation of X; NOT O = id (X \ (dom O))
let z, s be object ; RELAT_1:def 2 ( ( not [z,s] in NOT O or [z,s] in id (X \ (dom O)) ) & ( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O ) )
thus
( [z,s] in NOT O implies [z,s] in id (X \ (dom O)) )
( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O )
assume
[z,s] in id (X \ (dom O))
; [z,s] in NOT O
then A2:
( z = s & z in X \ (dom O) )
by RELAT_1:def 10;
then
( z in X & z nin dom O )
by XBOOLE_0:def 5;
hence
[z,s] in NOT O
by A2, Th36; verum