theorem Th6: :: WAYBEL15:6

for L1, L2 being non empty Poset
for f being Function of L1,L2
for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds
( [f,f1] is Galois & [f1,f] is Galois )