let S, T be non empty Poset; :: thesis: for f1 being Function of S,T
for g1 being Function of T,S
for f2 being Function of (S ~ ),(T ~ )
for g2 being Function of (T ~ ),(S ~ ) st f1 = f2 & g1 = g2 holds
( [f1,g1] is Galois iff [g2,f2] is Galois )
let f1 be Function of S,T; :: thesis: for g1 being Function of T,S
for f2 being Function of (S ~ ),(T ~ )
for g2 being Function of (T ~ ),(S ~ ) st f1 = f2 & g1 = g2 holds
( [f1,g1] is Galois iff [g2,f2] is Galois )
let g1 be Function of T,S; :: thesis: for f2 being Function of (S ~ ),(T ~ )
for g2 being Function of (T ~ ),(S ~ ) st f1 = f2 & g1 = g2 holds
( [f1,g1] is Galois iff [g2,f2] is Galois )
let f2 be Function of (S ~ ),(T ~ ); :: thesis: for g2 being Function of (T ~ ),(S ~ ) st f1 = f2 & g1 = g2 holds
( [f1,g1] is Galois iff [g2,f2] is Galois )
let g2 be Function of (T ~ ),(S ~ ); :: thesis: ( f1 = f2 & g1 = g2 implies ( [f1,g1] is Galois iff [g2,f2] is Galois ) )
assume A1: ( f1 = f2 & g1 = g2 ) ; :: thesis: ( [f1,g1] is Galois iff [g2,f2] is Galois )

hereby :: thesis: ( [g2,f2] is Galois implies [f1,g1] is Galois )

assume A2: [f1,g1] is Galois ; :: thesis: [g2,f2] is Galois
then ( g1 is monotone & f1 is monotone & ( for t being Element of T
for s being Element of S holds
( t <= f1 . s iff g1 . t <= s ) ) ) by WAYBEL_1:9;
then A3: ( g2 is monotone & f2 is monotone ) by A1, Th42;

now

let s be Element of (S ~ ); :: thesis: for t being Element of (T ~ ) holds
( g2 . t >= s iff t >= f2 . s )
let t be Element of (T ~ ); :: thesis: ( g2 . t >= s iff t >= f2 . s )
( ~ s = s & ~ t = t & (f1 . (~ s)) ~ = f1 . (~ s) & (g1 . (~ t)) ~ = g1 . (~ t) & ( ~ t <= f1 . (~ s) implies g1 . (~ t) <= ~ s ) & ( g1 . (~ t) <= ~ s implies ~ t <= f1 . (~ s) ) ) by A2, WAYBEL_1:9;
hence ( g2 . t >= s iff t >= f2 . s ) by A1, Th2; :: thesis: verum

end;

hence [g2,f2] is Galois by A3, WAYBEL_1:9; :: thesis: verum

end;

assume A4: [g2,f2] is Galois ; :: thesis: [f1,g1] is Galois
then ( g2 is monotone & f2 is monotone & ( for s being Element of (S ~ )
for t being Element of (T ~ ) holds
( s <= g2 . t iff f2 . s <= t ) ) ) by WAYBEL_1:9;
then A5: ( g1 is monotone & f1 is monotone ) by A1, Th42;

now

let t be Element of T; :: thesis: for s being Element of S holds
( t <= f1 . s iff g1 . t <= s )
let s be Element of S; :: thesis: ( t <= f1 . s iff g1 . t <= s )
( s ~ = s & t ~ = t & ~ (f2 . (s ~ )) = f2 . (s ~ ) & ~ (g2 . (t ~ )) = g2 . (t ~ ) & ( s ~ <= g2 . (t ~ ) implies f2 . (s ~ ) <= t ~ ) & ( f2 . (s ~ ) <= t ~ implies s ~ <= g2 . (t ~ ) ) ) by A4, WAYBEL_1:9;
hence ( t <= f1 . s iff g1 . t <= s ) by A1, Th2; :: thesis: verum

end;

hence [f1,g1] is Galois by A5, WAYBEL_1:9; :: thesis: verum