let P, R be non empty Poset; :: thesis: for Con being Connection of P,R
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let Con be Connection of P,R; :: thesis: for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let f be Function of P,R; :: thesis: for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let g be Function of R,P; :: thesis: ( Con = [f,g] implies ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) )
assume A1: Con = [f,g] ; :: thesis: ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )

A2: now :: thesis: ( ( for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) implies Con is co-Galois )

assume A3: for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ; :: thesis: Con is co-Galois
for p1, p2 being Element of P st p1 <= p2 holds
for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2

proof

let p1, p2 be Element of P; :: thesis: ( p1 <= p2 implies for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2 )
assume A4: p1 <= p2 ; :: thesis: for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2
let r1, r2 be Element of R; :: thesis: ( r1 = f . p1 & r2 = f . p2 implies r1 >= r2 )
assume A5: ( r1 = f . p1 & r2 = f . p2 ) ; :: thesis: r1 >= r2
p2 <= g . (f . p2) by A3;
then p1 <= g . (f . p2) by A4, ORDERS_2:3;
hence r1 >= r2 by A3, A5; :: thesis: verum

end;

then A6: f is antitone by WAYBEL_0:def 5;
for r1, r2 being Element of R st r1 <= r2 holds
for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2

proof

let r1, r2 be Element of R; :: thesis: ( r1 <= r2 implies for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2 )
assume A7: r1 <= r2 ; :: thesis: for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2
let p1, p2 be Element of P; :: thesis: ( p1 = g . r1 & p2 = g . r2 implies p1 >= p2 )
assume A8: ( p1 = g . r1 & p2 = g . r2 ) ; :: thesis: p1 >= p2
r2 <= f . (g . r2) by A3;
then r1 <= f . (g . r2) by A7, ORDERS_2:3;
hence p1 >= p2 by A3, A8; :: thesis: verum

end;

then A9: g is antitone by WAYBEL_0:def 5;
for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) by A3;
hence Con is co-Galois by A1, A6, A9; :: thesis: verum

end;

now :: thesis: ( Con is co-Galois implies for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )

assume Con is co-Galois ; :: thesis: for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p )
then consider f9 being Function of P,R, g9 being Function of R,P such that
A10: Con = [f9,g9] and
A11: f9 is antitone and
A12: g9 is antitone and
A13: for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) ;
A14: g = [f,g] `2
.= Con `2 by A1
.= [f9,g9] `2 by A10
.= g9 ;
A15: f = [f,g] `1
.= Con `1 by A1
.= [f9,g9] `1 by A10
.= f9 ;
A16: for p being Element of P
for r being Element of R st r <= f . p holds
p <= g . r

proof

let p be Element of P; :: thesis: for r being Element of R st r <= f . p holds
p <= g . r
let r be Element of R; :: thesis: ( r <= f . p implies p <= g . r )
assume r <= f . p ; :: thesis: p <= g . r
then A17: g . r >= g . (f . p) by A12, A14, WAYBEL_0:def 5;
p <= g . (f . p) by A13, A15, A14;
hence p <= g . r by A17, ORDERS_2:3; :: thesis: verum

end;

for p being Element of P
for r being Element of R st p <= g . r holds
r <= f . p

proof

let p be Element of P; :: thesis: for r being Element of R st p <= g . r holds
r <= f . p
let r be Element of R; :: thesis: ( p <= g . r implies r <= f . p )
assume p <= g . r ; :: thesis: r <= f . p
then A18: f . p >= f . (g . r) by A11, A15, WAYBEL_0:def 5;
r <= f . (g . r) by A13, A15, A14;
hence r <= f . p by A18, ORDERS_2:3; :: thesis: verum

end;

hence for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) by A16; :: thesis: verum

end;

hence ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) by A2; :: thesis: verum