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