take
LSeg (|[0,0]|,|[0,1]|)
; ( 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:52;
hence
( LSeg (|[0,0]|,|[0,1]|) is compact & not LSeg (|[0,0]|,|[0,1]|) is empty & LSeg (|[0,0]|,|[0,1]|) is vertical )
by Th16; verum