:: deftheorem Def8 defines min-classes DICKSON:def 8 :
for R being non empty RelStr
for N being Subset of R
for b₃ being Subset-Family of R holds
( b₃ = min-classes N iff for x being set holds
( x in b₃ iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) );