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

( 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