let X be set ; :: thesis: for O being Operation of X holds NOT (NOT (NOT O)) = NOT O
let O be Operation of X; :: thesis: NOT (NOT (NOT O)) = NOT O
thus NOT (NOT (NOT O)) = id (X \ (dom (NOT (NOT O)))) by Th37
.= id (X \ (dom O)) by Th38
.= NOT O by Th37 ; :: thesis: verum