:: deftheorem defines -petit CLASSES5:def 15 :
for U being Universe
for G being Group holds
( G is U -petit iff ex g being Group st
( g is U -element & G,g are_isomorphic ) );