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

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 f' being Function of P,R, g' being Function of R,P such that
A3: ( Con = [f',g'] & f' is antitone & g' is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g' . (f' . p1) & r1 <= f' . (g' . r1) ) ) ) by Def10;
A4: f = Con `1 by A1, MCART_1:def 1
.= f' by A3, MCART_1:def 1 ;
A5: g = Con `2 by A1, MCART_1:def 2
.= g' by A3, MCART_1:def 2 ;
A6: 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 A7: f . p >= f . (g . r) by A3, A4, WAYBEL_0:def 5;
r <= f . (g . r) by A3, A4, A5;
hence r <= f . p by A7, ORDERS_2:26; :: thesis: verum

end;

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 A8: g . r >= g . (f . p) by A3, A5, WAYBEL_0:def 5;
p <= g . (f . p) by A3, A4, A5;
hence p <= g . r by A8, ORDERS_2:26; :: 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 A6; :: thesis: verum

end;

now

assume A9: 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
then A10: for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ;
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 A11: 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 A12: ( r1 = f . p1 & r2 = f . p2 ) ; :: thesis: r1 >= r2
p2 <= g . (f . p2) by A9;
then p1 <= g . (f . p2) by A11, ORDERS_2:26;
hence r1 >= r2 by A9, A12; :: thesis: verum

end;

then A13: 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 A14: 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 A15: ( p1 = g . r1 & p2 = g . r2 ) ; :: thesis: p1 >= p2
r2 <= f . (g . r2) by A9;
then r1 <= f . (g . r2) by A14, ORDERS_2:26;
hence p1 >= p2 by A9, A15; :: thesis: verum

end;

then g is antitone by WAYBEL_0:def 5;
hence Con is co-Galois by A1, A10, A13, Def10; :: 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