:: deftheorem Def2 defines Circled-Family CIRCLED1:def 2 :
for V being non empty RLSStruct
for M being Subset of V
for b₃ being Subset-Family of V holds
( b₃ = Circled-Family M iff for N being Subset of V holds
( N in b₃ iff ( N is circled & M c= N ) ) );