let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )
let B be with_bottom CLbasis of L; :: thesis: ( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )
[(supMap (subrelstr B)),(baseMap B)] is Galois by Th63;
hence ( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint ) by WAYBEL_1:9; :: thesis: verum