take LSeg |[0 ,0 ]|,|[1,0 ]| ; :: thesis: ( LSeg |[0 ,0 ]|,|[1,0 ]| is compact & not LSeg |[0 ,0 ]|,|[1,0 ]| is empty & LSeg |[0 ,0 ]|,|[1,0 ]| is horizontal )
( |[0 ,0 ]| `2 = 0 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
hence ( LSeg |[0 ,0 ]|,|[1,0 ]| is compact & not LSeg |[0 ,0 ]|,|[1,0 ]| is empty & LSeg |[0 ,0 ]|,|[1,0 ]| is horizontal ) by Th28, Th36; :: thesis: verum