set S = SingleMSS x;
let A1, A2 be strict Boolean MSAlgebra over SingleMSS x; :: thesis: A1 = A2
A1: the Sorts of A1 = the carrier of (SingleMSS x) --> BOOLEAN by CIRCCOMB:57;
A2: the Charact of A1 = {} ;
the Charact of A2 = {} ;
hence A1 = A2 by A1, A2, CIRCCOMB:57; :: thesis: verum