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