let S1, S2 be non empty non void ManySortedSign ; :: thesis: for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 tolerates A2 holds
A2 tolerates A1
let A1 be MSAlgebra of S1; :: thesis: for A2 being MSAlgebra of S2 st A1 tolerates A2 holds
A2 tolerates A1
let A2 be MSAlgebra of S2; :: thesis: ( A1 tolerates A2 implies A2 tolerates A1 )
assume that
A1: S1 tolerates S2 and
A2: the Sorts of A1 tolerates the Sorts of A2 and
A3: the Charact of A1 tolerates the Charact of A2 ; :: according to CIRCCOMB:def 3 :: thesis: A2 tolerates A1
thus ( S2 tolerates S1 & the Sorts of A2 tolerates the Sorts of A1 & the Charact of A2 tolerates the Charact of A1 ) by A1, A2, A3; :: according to CIRCCOMB:def 3 :: thesis: verum