theorem Th19: :: WAYBEL12:19

for L being non empty RelStr
for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds
S c= V