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

( 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