theorem Th4: :: WAYBEL15:4

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is onto & [g,d] is Galois holds
T, Image d are_isomorphic