let S, T, S', T' be non empty RelStr ; :: thesis: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) implies for c being Connection of S,T
for c' being Connection of S',T' st c = c' & c is Galois holds
c' is Galois )
assume that
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) and
A2: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) ; :: thesis: for c being Connection of S,T
for c' being Connection of S',T' st c = c' & c is Galois holds
c' is Galois
let c be Connection of S,T; :: thesis: for c' being Connection of S',T' st c = c' & c is Galois holds
c' is Galois
let c' be Connection of S',T'; :: thesis: ( c = c' & c is Galois implies c' is Galois )
assume A3: c = c' ; :: thesis: ( not c is Galois or c' 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: c' is Galois
reconsider g' = g as Function of S',T' by A1, A2;
reconsider d' = d as Function of T',S' by A1, A2;
take g' ; :: according to WAYBEL_1:def 10 :: thesis: ex b₁ being Element of bool [:the carrier of T',the carrier of S':] st
( c' = [g',b₁] & g' is monotone & b₁ is monotone & ( for b₂ being Element of the carrier of T'
for b₃ being Element of the carrier of S' holds
( ( not b₂ <= g' . b₃ or b₁ . b₂ <= b₃ ) & ( not b₁ . b₂ <= b₃ or b₂ <= g' . b₃ ) ) ) )
take d' ; :: thesis: ( c' = [g',d'] & g' is monotone & d' is monotone & ( for b₁ being Element of the carrier of T'
for b₂ being Element of the carrier of S' holds
( ( not b₁ <= g' . b₂ or d' . b₁ <= b₂ ) & ( not d' . b₁ <= b₂ or b₁ <= g' . b₂ ) ) ) )
thus c' = [g',d'] by A3, A4; :: thesis: ( g' is monotone & d' is monotone & ( for b₁ being Element of the carrier of T'
for b₂ being Element of the carrier of S' holds
( ( not b₁ <= g' . b₂ or d' . b₁ <= b₂ ) & ( not d' . b₁ <= b₂ or b₁ <= g' . b₂ ) ) ) )
thus ( g' is monotone & d' is monotone ) by A1, A2, A5, A6, WAYBEL_9:1; :: thesis: for b₁ being Element of the carrier of T'
for b₂ being Element of the carrier of S' holds
( ( not b₁ <= g' . b₂ or d' . b₁ <= b₂ ) & ( not d' . b₁ <= b₂ or b₁ <= g' . b₂ ) )
let t' be Element of T'; :: thesis: for b₁ being Element of the carrier of S' holds
( ( not t' <= g' . b₁ or d' . t' <= b₁ ) & ( not d' . t' <= b₁ or t' <= g' . b₁ ) )
let s' be Element of S'; :: thesis: ( ( not t' <= g' . s' or d' . t' <= s' ) & ( not d' . t' <= s' or t' <= g' . s' ) )
reconsider t = t' as Element of T by A2;
reconsider s = s' as Element of S by A1;
A8: ( t' <= g' . s' iff t <= g . s ) by A2, YELLOW_0:1;
( d' . t' <= s' iff d . t <= s ) by A1, YELLOW_0:1;
hence ( ( not t' <= g' . s' or d' . t' <= s' ) & ( not d' . t' <= s' or t' <= g' . s' ) ) by A7, A8; :: thesis: verum