let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; :: thesis: for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den holds
A1 tolerates A2
let A1 be MSAlgebra of S1; :: thesis: for A2 being MSAlgebra of S2 st A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den holds
A1 tolerates A2
let A2 be MSAlgebra of S2; :: thesis: ( A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den implies A1 tolerates A2 )
assume ( A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den ) ; :: thesis: A1 tolerates A2
hence ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) by Th55, Th56, Th67; :: according to CIRCCOMB:def 3 :: thesis: verum