theorem Th1: :: WAYBEL34:1

for S, T, S9, T9 being non empty RelStr st 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 #) holds
for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois