take [.0,1.[ ; :: thesis: ( [.0,1.[ is left_end & not [.0,1.[ is right_end & [.0,1.[ is interval )
thus ( [.0,1.[ is left_end & not [.0,1.[ is right_end & [.0,1.[ is interval ) by Th34; :: thesis: verum