:: deftheorem defines Galois WAYBEL_1:def 10 :
for S, T being non empty RelStr
for gc being Connection of S,T holds
( gc is Galois iff ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) );