theorem :: YELLOW_2:2

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