take f = I === ; :: thesis: f is I -extension
thus f is I -extension ; :: thesis: verum