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 )

then f2 is monotone by WAYBEL_1:8;

then A8: f1 is monotone by A1, Th42;

then g1 is monotone by A2, Th42;

hence [f1,g1] is Galois by A8, A9; :: thesis: verum

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 A7:
[g2,f2] is Galois
; :: thesis: [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;

then g2 is monotone by A2, Th42;

hence [g2,f2] is Galois by A4, A5; :: thesis: verum

end;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 )

g1 is monotone
by A3, WAYBEL_1:8;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;( 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

then g2 is monotone by A2, Th42;

hence [g2,f2] is Galois by A4, A5; :: thesis: verum

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 )

g2 is monotone
by A7, WAYBEL_1:8;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;( 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

then g1 is monotone by A2, Th42;

hence [f1,g1] is Galois by A8, A9; :: thesis: verum