take ].0,1.[ ; :: thesis: ].0,1.[ is open
thus ].0,1.[ is open ; :: thesis: verum