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