take I[01] ; :: thesis: ( not I[01] is empty & I[01] is real-membered )
thus ( not I[01] is empty & I[01] is real-membered ) ; :: thesis: verum