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