pi X,i c= the carrier of (EqRelLatt (M . i))

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in pi X,i or z in the carrier of (EqRelLatt (M . i)) )
assume z in pi X,i ; :: thesis: z in the carrier of (EqRelLatt (M . i))
then consider f being Function such that
A1: f in X and
A2: z = f . i by CARD_3:def 6;
reconsider f = f as Equivalence_Relation of M by A1, MSUALG_5:def 5;
f . i is Equivalence_Relation of (M . i) by MSUALG_4:def 3;
hence z in the carrier of (EqRelLatt (M . i)) by A2, MSUALG_7:1; :: thesis: verum

end;

hence EqRelSet , is Subset of (EqRelLatt (M . i)) ; :: thesis: verum