theorem Th35: :: WAYBEL_2:35

for S being non empty RelStr
for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2