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 that
A1: f1 = f2 and
A2: g1 = g2 ; :: thesis: ( [f1,g1] is Galois iff [g2,f2] is Galois )

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

assume A3: [f1,g1] is Galois ; :: thesis: [g2,f2] is Galois
then f1 is monotone by WAYBEL_1:8;
then A4: f2 is monotone by A1, Th42;

A5: now :: thesis: for s being Element of (S ~)
for t being Element of (T ~) holds
( g2 . t >= s iff t >= f2 . s )

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 )
A6: ( (f1 . (~ s)) ~ = f1 . (~ s) & (g1 . (~ t)) ~ = g1 . (~ t) ) ;
( ~ t <= f1 . (~ s) iff g1 . (~ t) <= ~ s ) by A3, WAYBEL_1:8;
hence ( g2 . t >= s iff t >= f2 . s ) by A1, A2, A6, Th2; :: thesis: verum

end;

g1 is monotone by A3, WAYBEL_1:8;
then g2 is monotone by A2, Th42;
hence [g2,f2] is Galois by A4, A5; :: thesis: verum

end;

assume A7: [g2,f2] is Galois ; :: thesis: [f1,g1] is Galois
then f2 is monotone by WAYBEL_1:8;
then A8: f1 is monotone by A1, Th42;

A9: now :: thesis: for t being Element of T
for s being Element of S holds
( t <= f1 . s iff g1 . t <= s )

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 )
A10: ( ~ (f2 . (s ~)) = f2 . (s ~) & ~ (g2 . (t ~)) = g2 . (t ~) ) ;
( s ~ <= g2 . (t ~) iff f2 . (s ~) <= t ~ ) by A7, WAYBEL_1:8;
hence ( t <= f1 . s iff g1 . t <= s ) by A1, A2, A10, Th2; :: thesis: verum

end;

g2 is monotone by A7, WAYBEL_1:8;
then g1 is monotone by A2, Th42;
hence [f1,g1] is Galois by A8, A9; :: thesis: verum