let L1, L2, L3 be complete LATTICE; :: thesis: for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
let d1 be sups-preserving Function of L1,L2; :: thesis: for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
let d2 be sups-preserving Function of L2,L3; :: thesis: UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
A1: [(UpperAdj d1),d1] is Galois by Def2;
[(UpperAdj d2),d2] is Galois by Def2;
then A2: [((UpperAdj d1) * (UpperAdj d2)),(d2 * d1)] is Galois by A1, WAYBEL15:5;
d2 * d1 is sups-preserving by WAYBEL20:27;
hence UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2) by A2, Def2; :: thesis: verum