consider f being non constant standard special_circular_sequence;
take L~ f ; :: thesis: ( L~ f is compact & not L~ f is vertical & not L~ f is horizontal & L~ f is being_simple_closed_curve & not L~ f is empty )
thus ( L~ f is compact & not L~ f is vertical & not L~ f is horizontal & L~ f is being_simple_closed_curve & not L~ f is empty ) ; :: thesis: verum