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 A1, A2, WAYBEL_0:68;

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 A1, A2, FUNCT_1:39
.= 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 A3, WAYBEL_1:def 2;
then f1 . t <= (f1 * f) . s by A4, FUNCT_1:13;
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 A1, A2, FUNCT_1:39
.= id L2 by A2, WAYBEL_0:66 ;
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 A2, WAYBEL_1:def 2;
then (f * f1) . t <= f . s by A6, FUNCT_1:13;
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 A1, A2, FUNCT_1:39
.= id L2 by A2, WAYBEL_0:66 ;
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 A2, WAYBEL_1:def 2;
then f . t <= (f * f1) . s by A8, FUNCT_1:13;
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 A1, A2, FUNCT_1:39
.= 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 A3, WAYBEL_1:def 2;
then (f1 * f) . t <= f1 . s by A10, FUNCT_1:13;
hence t <= f1 . s by A11; :: thesis: verum

end;

end;

hence [f1,f] is Galois by A2, A3; :: thesis: verum