for B being non empty non void bool-correct BoolSignature
for A1 being non-empty bool-correct MSAlgebra over B
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct