let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2
for A3 being MSAlgebra of S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A1 be non-empty MSAlgebra of S1; :: thesis: for A2 being non-empty MSAlgebra of S2
for A3 being MSAlgebra of S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A2 be non-empty MSAlgebra of S2; :: thesis: for A3 being MSAlgebra of S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A3 be MSAlgebra of S3; :: thesis: ( A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 implies A1 +* A2 tolerates A3 )
assume that
A1: ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) and
A2: ( S2 tolerates S3 & the Sorts of A2 tolerates the Sorts of A3 & the Charact of A2 tolerates the Charact of A3 ) and
A3: ( S3 tolerates S1 & the Sorts of A3 tolerates the Sorts of A1 & the Charact of A3 tolerates the Charact of A1 ) ; :: according to CIRCCOMB:def 3 :: thesis: A1 +* A2 tolerates A3
thus S1 +* S2 tolerates S3 by A1, A2, A3, Th7; :: according to CIRCCOMB:def 3 :: thesis: ( the Sorts of (A1 +* A2) tolerates the Sorts of A3 & the Charact of (A1 +* A2) tolerates the Charact of A3 )
the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by A1, Def4;
hence the Sorts of (A1 +* A2) tolerates the Sorts of A3 by A1, A2, A3, Th5; :: thesis: the Charact of (A1 +* A2) tolerates the Charact of A3
the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A1, Def4;
hence the Charact of (A1 +* A2) tolerates the Charact of A3 by A1, A2, A3, Th5; :: thesis: verum