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

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