set O = the Operation of X;
take NOT the Operation of X ; :: thesis: NOT the Operation of X is filtering
thus NOT the Operation of X is filtering ; :: thesis: verum