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