theorem Th64: :: WAYBEL23:64

for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )