let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra of S holds
( A is Boolean iff rng the Sorts of A c= {BOOLEAN } )
let A be MSAlgebra of S; :: thesis: ( A is Boolean iff rng the Sorts of A c= {BOOLEAN } )

hereby :: thesis: ( rng the Sorts of A c= {BOOLEAN } implies A is Boolean )

assume A is Boolean ; :: thesis: rng the Sorts of A c= {BOOLEAN }
then the Sorts of A = the carrier of S --> BOOLEAN by Th65;
hence rng the Sorts of A c= {BOOLEAN } by FUNCOP_1:19; :: thesis: verum

end;

assume A1: rng the Sorts of A c= {BOOLEAN } ; :: thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def 15 :: thesis: the Sorts of A . v = BOOLEAN
dom the Sorts of A = the carrier of S by PARTFUN1:def 4;
then the Sorts of A . v in rng the Sorts of A by FUNCT_1:def 5;
hence the Sorts of A . v = BOOLEAN by A1, TARSKI:def 1; :: thesis: verum