seq_logn in Big_Oh (seq_n^ (1 / 2)) by Th4, Th5;
hence ( seq_n^ (1 / 2) in Big_Omega seq_logn & not seq_logn in Big_Omega (seq_n^ (1 / 2)) ) by Th4, Th5, ASYMPT_0:19; :: thesis: verum