theorem :: CONLAT_1:13

for P, R being non empty Poset
for Con being Connection of P,R st Con is co-Galois holds
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )