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 A1: ( 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' #) ) ; :: 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 A2: 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 A3: c = [g,d] and
A4: ( g is monotone & d is monotone ) and
A5: 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;
reconsider d' = d as Function of T',S' by A1;
take g' ; :: according to WAYBEL_1:def 10 :: thesis: ex b₁ being Relation of 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 A2, A3; :: 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, A4, 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 A1;
reconsider s = s' as Element of S by A1;
( ( t' <= g' . s' implies t <= g . s ) & ( t <= g . s implies t' <= g' . s' ) & ( d' . t' <= s' implies d . t <= s ) & ( d . t <= s implies 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 A5; :: thesis: verum