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 Th5
.= id (X \ (dom O)) by Th6
.= NOT O by Th5 ; :: thesis: verum