let L1, L2, L3 be non empty Poset; for g1 being Function of L1,L2
for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let g1 be Function of L1,L2; for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let g2 be Function of L2,L3; for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let d1 be Function of L2,L1; for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let d2 be Function of L3,L2; ( [g1,d1] is Galois & [g2,d2] is Galois implies [(g2 * g1),(d1 * d2)] is Galois )
assume that
A1:
[g1,d1] is Galois
and
A2:
[g2,d2] is Galois
; [(g2 * g1),(d1 * d2)] is Galois
A3:
d1 is monotone
by A1, WAYBEL_1:8;
A4:
g2 is monotone
by A2, WAYBEL_1:8;
A5:
now for s being Element of L3
for t being Element of L1 holds
( ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) & ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) )end;
d2 is monotone
by A2, WAYBEL_1:8;
then A10:
d1 * d2 is monotone
by A3, YELLOW_2:12;
g1 is monotone
by A1, WAYBEL_1:8;
then
g2 * g1 is monotone
by A4, YELLOW_2:12;
hence
[(g2 * g1),(d1 * d2)] is Galois
by A10, A5; verum