theorem Th25: :: YELLOW12:25

for R being lower-bounded sup-Semilattice
for X being Subset of [:R,R:] st ex_sup_of (sup_op R) .: X,R holds
sup_op R preserves_sup_of X