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 )
A1: SupMap L is sups-preserving by WAYBEL13:33;
thus supMap (subrelstr B) is infs-preserving by Th64, WAYBEL_1:12; :: thesis: supMap (subrelstr B) is sups-preserving
A2: supMap (subrelstr B) = (SupMap L) * (idsMap (subrelstr B)) by Th62;
idsMap (subrelstr B) is sups-preserving by Th61;
hence supMap (subrelstr B) is sups-preserving by A2, A1, WAYBEL20:27; :: thesis: verum