let G be _Graph; :: thesis: ( G is n + 3 -vertex & G is complete implies not G is acyclic )
assume A1: ( G is n + 3 -vertex & G is complete ) ; :: thesis: not G is acyclic
3 + 0 <= 3 + n by XREAL_1:6;
then 3 c= n + 3 by FIELD_5:3;
hence not G is acyclic by A1, Th8; :: thesis: verum