let X be set ; :: thesis: for O being Operation of X holds dom (NOT (NOT O)) = dom O
let O be Operation of X; :: thesis: dom (NOT (NOT O)) = dom O
thus dom (NOT (NOT O)) = dom (id (X \ (dom (NOT O)))) by Th5
.= X \ (dom (NOT O)) by RELAT_1:45
.= X \ (dom (id (X \ (dom O)))) by Th5
.= X \ (X \ (dom O)) by RELAT_1:45
.= X /\ (dom O) by XBOOLE_1:48
.= dom O by XBOOLE_1:28 ; :: thesis: verum