let X be set ; :: thesis: for O being Operation of X holds O AND (NOT O) = {}
let O be Operation of X; :: thesis: O AND (NOT O) = {}
dom (O AND (NOT O)) = dom (O /\ (id (X \ (dom O)))) by Th37;
then A1: dom (O AND (NOT O)) c= (dom O) /\ (dom (id (X \ (dom O)))) by XTUPLE_0:24;
(dom O) /\ (dom (id (X \ (dom O)))) = (dom O) /\ (X \ (dom O)) by RELAT_1:45
.= ((dom O) /\ X) \ (dom O) by XBOOLE_1:49
.= (dom O) \ (dom O) by XBOOLE_1:28
.= {} by XBOOLE_1:37 ;
hence O AND (NOT O) = {} by A1, RELAT_1:41, XBOOLE_1:3; :: thesis: verum