take ].0,1.[ ; :: thesis: ( ].0,1.[ is open & ].0,1.[ is real-bounded & ].0,1.[ is interval & not ].0,1.[ is empty )
thus ( ].0,1.[ is open & ].0,1.[ is real-bounded & ].0,1.[ is interval & not ].0,1.[ is empty ) ; :: thesis: verum