let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )
let B be with_bottom CLbasis of L; :: thesis: ( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )
supMap (subrelstr B) is upper_adjoint by Th64;
hence supMap (subrelstr B) is infs-preserving by WAYBEL_1:13; :: thesis: supMap (subrelstr B) is sups-preserving
A1: idsMap (subrelstr B) is sups-preserving by Th61;
A2: supMap (subrelstr B) = (SupMap L) * (idsMap (subrelstr B)) by Th62;
SupMap L is sups-preserving by WAYBEL13:33;
hence supMap (subrelstr B) is sups-preserving by A1, A2, WAYBEL20:28; :: thesis: verum