:: deftheorem defines co-Galois CONLAT_1:def 7 :
for P, R being non empty RelStr
for Con being Connection of P,R holds
( Con is co-Galois iff ex f being Function of P,R ex g being Function of R,P st
( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ) );