theorem :: WAYBEL12:20

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