theorem Th44: :: YELLOW10:44

for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]