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