let z be object ; :: 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 2;
hence z in the carrier of (EqRelLatt (M . i)) by A2, MSUALG_5:21; :: thesis: verum