theorem Th59: :: WAYBEL_1:59

for S being non empty RelStr
for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)