:: deftheorem defines with_max's TAXONOM2:def 8 :
for Y being set
for F being Subset-Family of Y holds
( F is with_max's iff for S being Subset of Y st S in F holds
ex T being Subset of Y st
( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds
V = Y ) ) );