let L1, L2 be non empty Poset; :: thesis: 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 )

let f be Function of L1,L2; :: thesis: for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds
( [f,f1] is Galois & [f1,f] is Galois )

let f1 be Function of L2,L1; :: thesis: ( f1 = f " & f is isomorphic implies ( [f,f1] is Galois & [f1,f] is Galois ) )
assume that
A1: f1 = f " and
A2: f is isomorphic ; :: thesis: ( [f,f1] is Galois & [f1,f] is Galois )
A3: f1 is isomorphic by ;
now :: thesis: for t being Element of L2
for s being Element of L1 holds
( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )
let t be Element of L2; :: thesis: for s being Element of L1 holds
( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

let s be Element of L1; :: thesis: ( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )
s in the carrier of L1 ;
then A4: s in dom f by FUNCT_2:def 1;
A5: f1 * f = id (dom f) by
.= id L1 by FUNCT_2:def 1 ;
thus ( t <= f . s implies f1 . t <= s ) :: thesis: ( f1 . t <= s implies t <= f . s )
proof
assume t <= f . s ; :: thesis: f1 . t <= s
then f1 . t <= f1 . (f . s) by ;
then f1 . t <= (f1 * f) . s by ;
hence f1 . t <= s by A5; :: thesis: verum
end;
t in the carrier of L2 ;
then A6: t in dom f1 by FUNCT_2:def 1;
A7: f * f1 = id (rng f) by
.= id L2 by ;
thus ( f1 . t <= s implies t <= f . s ) :: thesis: verum
proof
assume f1 . t <= s ; :: thesis: t <= f . s
then f . (f1 . t) <= f . s by ;
then (f * f1) . t <= f . s by ;
hence t <= f . s by A7; :: thesis: verum
end;
end;
hence [f,f1] is Galois by A2, A3; :: thesis: [f1,f] is Galois
now :: thesis: for t being Element of L1
for s being Element of L2 holds
( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )
let t be Element of L1; :: thesis: for s being Element of L2 holds
( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

let s be Element of L2; :: thesis: ( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )
s in the carrier of L2 ;
then A8: s in dom f1 by FUNCT_2:def 1;
A9: f * f1 = id (rng f) by
.= id L2 by ;
thus ( t <= f1 . s implies f . t <= s ) :: thesis: ( f . t <= s implies t <= f1 . s )
proof
assume t <= f1 . s ; :: thesis: f . t <= s
then f . t <= f . (f1 . s) by ;
then f . t <= (f * f1) . s by ;
hence f . t <= s by A9; :: thesis: verum
end;
t in the carrier of L1 ;
then A10: t in dom f by FUNCT_2:def 1;
A11: f1 * f = id (dom f) by
.= id L1 by FUNCT_2:def 1 ;
thus ( f . t <= s implies t <= f1 . s ) :: thesis: verum
proof
assume f . t <= s ; :: thesis: t <= f1 . s
then f1 . (f . t) <= f1 . s by ;
then (f1 * f) . t <= f1 . s by ;
hence t <= f1 . s by A11; :: thesis: verum
end;
end;
hence [f1,f] is Galois by A2, A3; :: thesis: verum