let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra over S holds
( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )
let A be MSAlgebra over 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 Th57;
hence rng the Sorts of A c= {BOOLEAN} by FUNCOP_1:13; :: 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 14 :: thesis: the Sorts of A . v = BOOLEAN
dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
then the Sorts of A . v in rng the Sorts of A by FUNCT_1:def 3;
hence the Sorts of A . v = BOOLEAN by A1, TARSKI:def 1; :: thesis: verum