:: deftheorem defines |^ GROUP_3:def 3 :
for G being Group
for A, B being Subset of G holds A |^ B = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;