take ].0,2.[ ; :: thesis: ( not ].0,2.[ is left_end & not ].0,2.[ is right_end & ].0,2.[ is interval & 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 interval & not ].0,2.[ is empty ) ; :: thesis: verum