thus for Y being Subset of (EqRelLatt (M . i)) holds
( Y = pi (X,i) iff for x being set holds
( x in Y iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) ) :: thesis:

let Y be Subset of (EqRelLatt (M . i)); :: thesis:
thus ( Y = pi (X,i) implies for x being set holds
( x in Y iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) ) :: thesis:

assume A3: Y = pi (X,i) ; :: thesis:
let x be set ; :: thesis:
thus ( x in Y implies ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) :: thesis:

assume x in Y ; :: thesis:
then consider f being Function such that
A4: f in X and
A5: x = f . i by A3, CARD_3:def 6;
reconsider f = f as Equivalence_Relation of M by A4, MSUALG_5:def 5;
take f ; :: thesis:
thus ( x = f . i & f in X ) by A4, A5; :: thesis:

end;

end;

thus ( ( for x being set holds
( x in Y iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) ) implies Y = pi (X,i) ) :: thesis:

assume A6: for x being set holds
( x in Y iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) ; :: thesis:
thus Y c= pi (X,i) :: according to XBOOLE_0:def 10 :: thesis:

end;

thus pi (X,i) c= Y :: thesis:

let y1 be object ; :: according to TARSKI:def 3 :: thesis:
assume y1 in pi (X,i) ; :: thesis:
then consider f being Function such that
A7: f in X and
A8: y1 = f . i by CARD_3:def 6;
reconsider f = f as Equivalence_Relation of M by A7, MSUALG_5:def 5;
ex Eq being Equivalence_Relation of M st
( y1 = Eq . i & Eq in X )

take f ; :: thesis:
thus ( y1 = f . i & f in X ) by A7, A8; :: thesis:

end;

end;