take ].0 ,2.[ ; :: thesis: ( not ].0 ,2.[ is left_end & not ].0 ,2.[ is right_end & ].0 ,2.[ is connected & not ].0 ,2.[ is empty )
1 in ].0 ,2.[ by XXREAL_1:4;
hence ( not ].0 ,2.[ is left_end & not ].0 ,2.[ is right_end & ].0 ,2.[ is connected & not ].0 ,2.[ is empty ) ; :: thesis: verum