let C1, C2 be strict SubLattice of EqRelLatt the Sorts of A; :: thesis: ( ( for x being set holds
( x in the carrier of C1 iff x is MSCongruence of A ) ) & ( for x being set holds
( x in the carrier of C2 iff x is MSCongruence of A ) ) implies C1 = C2 )
assume that
A33: for x being set holds
( x in the carrier of C1 iff x is MSCongruence of A ) and
A34: for x being set holds
( x in the carrier of C2 iff x is MSCongruence of A ) ; :: thesis: C1 = C2

A35: now

let x be set ; :: thesis: ( x in the carrier of C1 iff x in the carrier of C2 )
( x in the carrier of C2 iff x is MSCongruence of A ) by A34;
hence ( x in the carrier of C1 iff x in the carrier of C2 ) by A33; :: thesis: verum

end;

then A36: the carrier of C1 = the carrier of C2 by TARSKI:1;
then A37: the L_join of C1 = the L_join of (EqRelLatt the Sorts of A) || the carrier of C2 by NAT_LAT:def 12
.= the L_join of C2 by NAT_LAT:def 12 ;
the L_meet of C1 = the L_meet of (EqRelLatt the Sorts of A) || the carrier of C2 by A36, NAT_LAT:def 12
.= the L_meet of C2 by NAT_LAT:def 12 ;
hence C1 = C2 by A35, A37, TARSKI:1; :: thesis: verum