let S, T, S9, T9 be non empty RelStr ; ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) implies for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois )
assume that
A1:
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #)
and
A2:
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #)
; for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois
let c be Connection of S,T; for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois
let c9 be Connection of S9,T9; ( c = c9 & c is Galois implies c9 is Galois )
assume A3:
c = c9
; ( not c is Galois or c9 is Galois )
given g being Function of S,T, d being Function of T,S such that A4:
c = [g,d]
and
A5:
g is monotone
and
A6:
d is monotone
and
A7:
for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s )
; WAYBEL_1:def 10 c9 is Galois
reconsider g9 = g as Function of S9,T9 by A1, A2;
reconsider d9 = d as Function of T9,S9 by A1, A2;
take
g9
; WAYBEL_1:def 10 ex b1 being Element of bool [: the carrier of T9, the carrier of S9:] st
( c9 = [g9,b1] & g9 is monotone & b1 is monotone & ( for b2 being Element of the carrier of T9
for b3 being Element of the carrier of S9 holds
( ( not b2 <= g9 . b3 or b1 . b2 <= b3 ) & ( not b1 . b2 <= b3 or b2 <= g9 . b3 ) ) ) )
take
d9
; ( c9 = [g9,d9] & g9 is monotone & d9 is monotone & ( for b1 being Element of the carrier of T9
for b2 being Element of the carrier of S9 holds
( ( not b1 <= g9 . b2 or d9 . b1 <= b2 ) & ( not d9 . b1 <= b2 or b1 <= g9 . b2 ) ) ) )
thus
c9 = [g9,d9]
by A3, A4; ( g9 is monotone & d9 is monotone & ( for b1 being Element of the carrier of T9
for b2 being Element of the carrier of S9 holds
( ( not b1 <= g9 . b2 or d9 . b1 <= b2 ) & ( not d9 . b1 <= b2 or b1 <= g9 . b2 ) ) ) )
thus
( g9 is monotone & d9 is monotone )
by A1, A2, A5, A6, WAYBEL_9:1; for b1 being Element of the carrier of T9
for b2 being Element of the carrier of S9 holds
( ( not b1 <= g9 . b2 or d9 . b1 <= b2 ) & ( not d9 . b1 <= b2 or b1 <= g9 . b2 ) )
let t9 be Element of T9; for b1 being Element of the carrier of S9 holds
( ( not t9 <= g9 . b1 or d9 . t9 <= b1 ) & ( not d9 . t9 <= b1 or t9 <= g9 . b1 ) )
let s9 be Element of S9; ( ( not t9 <= g9 . s9 or d9 . t9 <= s9 ) & ( not d9 . t9 <= s9 or t9 <= g9 . s9 ) )
reconsider t = t9 as Element of T by A2;
reconsider s = s9 as Element of S by A1;
A8:
( t9 <= g9 . s9 iff t <= g . s )
by A2, YELLOW_0:1;
( d9 . t9 <= s9 iff d . t <= s )
by A1, YELLOW_0:1;
hence
( ( not t9 <= g9 . s9 or d9 . t9 <= s9 ) & ( not d9 . t9 <= s9 or t9 <= g9 . s9 ) )
by A7, A8; verum