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