take I[01] ; :: thesis: I[01] is real-membered
thus I[01] is real-membered ; :: thesis: verum