let X be set ; :: thesis: for O being Operation of X holds dom (O OR (NOT O)) = X
let O be Operation of X; :: thesis: dom (O OR (NOT O)) = X
thus dom (O OR (NOT O)) = (dom O) OR (dom (NOT O)) by XTUPLE_0:23
.= (dom O) \/ (dom (id (X \ (dom O)))) by Th37
.= (dom O) OR (X \ (dom O)) by RELAT_1:45
.= (dom O) \/ X by XBOOLE_1:39
.= X by XBOOLE_1:12 ; :: thesis: verum