:: deftheorem def1 defines upper CARDFIL2:def 1 :
for X being set
for SFX being Subset-Family of X holds
( SFX is upper iff for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX );