let S, T, S9, T9 be non empty RelStr ; :: thesis: ( 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 #) ; :: thesis: 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; :: thesis: for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois
let c9 be Connection of S9,T9; :: thesis: ( c = c9 & c is Galois implies c9 is Galois )
assume A3: c = c9 ; :: thesis: ( 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 ) ; :: according to WAYBEL_1:def 10 :: thesis: 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 ; :: according to WAYBEL_1:def 10 :: thesis: ex b₁ being Element of bool [: the carrier of T9, the carrier of S9:] st
( c9 = [g9,b₁] & g9 is monotone & b₁ is monotone & ( for b₂ being Element of the carrier of T9
for b₃ being Element of the carrier of S9 holds
( ( not b₂ <= g9 . b₃ or b₁ . b₂ <= b₃ ) & ( not b₁ . b₂ <= b₃ or b₂ <= g9 . b₃ ) ) ) )
take d9 ; :: thesis: ( c9 = [g9,d9] & g9 is monotone & d9 is monotone & ( for b₁ being Element of the carrier of T9
for b₂ being Element of the carrier of S9 holds
( ( not b₁ <= g9 . b₂ or d9 . b₁ <= b₂ ) & ( not d9 . b₁ <= b₂ or b₁ <= g9 . b₂ ) ) ) )
thus c9 = [g9,d9] by A3, A4; :: thesis: ( g9 is monotone & d9 is monotone & ( for b₁ being Element of the carrier of T9
for b₂ being Element of the carrier of S9 holds
( ( not b₁ <= g9 . b₂ or d9 . b₁ <= b₂ ) & ( not d9 . b₁ <= b₂ or b₁ <= g9 . b₂ ) ) ) )
thus ( g9 is monotone & d9 is monotone ) by A1, A2, A5, A6, WAYBEL_9:1; :: thesis: for b₁ being Element of the carrier of T9
for b₂ being Element of the carrier of S9 holds
( ( not b₁ <= g9 . b₂ or d9 . b₁ <= b₂ ) & ( not d9 . b₁ <= b₂ or b₁ <= g9 . b₂ ) )
let t9 be Element of T9; :: thesis: for b₁ being Element of the carrier of S9 holds
( ( not t9 <= g9 . b₁ or d9 . t9 <= b₁ ) & ( not d9 . t9 <= b₁ or t9 <= g9 . b₁ ) )
let s9 be Element of S9; :: thesis: ( ( 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; :: thesis: verum