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 Th37; :: thesis: verum