set S = SingleMSS x;
let A1, A2 be strict Boolean MSAlgebra of SingleMSS x; :: thesis: A1 = A2
( dom the Charact of A1 = {} & dom the Charact of A2 = {} ) by PARTFUN1:def 4;
then ( the Sorts of A1 = the carrier of (SingleMSS x) --> BOOLEAN & the Sorts of A2 = the carrier of (SingleMSS x) --> BOOLEAN & the Charact of A1 = {} & the Charact of A2 = {} ) by CIRCCOMB:65;
hence A1 = A2 ; :: thesis: verum