let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2
let A1 be MSAlgebra of S1; :: thesis: for A2 being MSAlgebra of S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2
let A2 be MSAlgebra of S2; :: thesis: ( A1 is Boolean & A2 is Boolean implies the Sorts of A1 tolerates the Sorts of A2 )
assume ( A1 is Boolean & A2 is Boolean ) ; :: thesis: the Sorts of A1 tolerates the Sorts of A2
then ( the Sorts of A1 = the carrier of S1 --> BOOLEAN & the Sorts of A2 = the carrier of S2 --> BOOLEAN ) by Th65;
hence the Sorts of A1 tolerates the Sorts of A2 by Th4; :: thesis: verum