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