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