theorem Th25: :: WAYBEL_1:25

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}