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