:: deftheorem defines Cir CIRCLED1:def 3 :
for V being RealLinearSpace
for M being Subset of V holds Cir M = meet (Circled-Family M);