let X be set ; :: thesis: for O being Operation of X holds NOT O = id (X \ (dom O))
let O be Operation of X; :: thesis: NOT O = id (X \ (dom O))
let z, s be object ; :: according to RELAT_1:def 2 :: thesis: ( ( 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)) ) :: thesis: ( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O )
proof
assume [z,s] in NOT O ; :: thesis: [z,s] in id (X \ (dom O))
then A1: ( z = s & z in X & z nin dom O ) by Th36;
then z in X \ (dom O) by XBOOLE_0:def 5;
hence [z,s] in id (X \ (dom O)) by A1, RELAT_1:def 10; :: thesis: verum
end;
assume [z,s] in id (X \ (dom O)) ; :: thesis: [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; :: thesis: verum