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