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
A34: now :: thesis: for x being object holds
( 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;
then A35: the carrier of C1 = the carrier of C2 by TARSKI:2;
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