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