theorem Th7: :: WAYBEL_7:7

for X being set
for Y being Subset of (BoolePoset X) holds
( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds
y in Y )