theorem :: YELLOW_2:1

for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= downarrow x iff X is_<=_than x ) by WAYBEL_0:17;