:: deftheorem Def13 defines the_fixed_points_of GROUP_10:def 13 :
for S being non empty unital multMagma
for E being set
for T being LeftOperation of S,E holds
( ( not E is empty implies the_fixed_points_of T = { x where x is Element of E : x is_fixed_under T } ) & ( E is empty implies the_fixed_points_of T = {} E ) );