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

A32: for x being set holds

( x in the carrier of C1 iff x is MSCongruence of A ) and

A33: for x being set holds

( x in the carrier of C2 iff x is MSCongruence of A ) ; :: thesis: C1 = C2

then A36: 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 A35, NAT_LAT:def 12

.= the L_meet of C2 by NAT_LAT:def 12 ;

hence C1 = C2 by A34, A36, TARSKI:2; :: thesis: verum

( 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

A32: for x being set holds

( x in the carrier of C1 iff x is MSCongruence of A ) and

A33: for x being set holds

( x in the carrier of C2 iff x is MSCongruence of A ) ; :: thesis: C1 = C2

A34: now :: thesis: for x being object holds

( x in the carrier of C1 iff x in the carrier of C2 )

then A35:
the carrier of C1 = the carrier of C2
by TARSKI:2;( x in the carrier of C1 iff x in the carrier of C2 )

let x be object ; :: 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 A33;

hence ( x in the carrier of C1 iff x in the carrier of C2 ) by A32; :: thesis: verum

end;( x in the carrier of C2 iff x is MSCongruence of A ) by A33;

hence ( x in the carrier of C1 iff x in the carrier of C2 ) by A32; :: thesis: verum

then A36: 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 A35, NAT_LAT:def 12

.= the L_meet of C2 by NAT_LAT:def 12 ;

hence C1 = C2 by A34, A36, TARSKI:2; :: thesis: verum