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