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