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: verum

proof

let Y be Subset of (EqRelLatt (M . i)); :: thesis: ( 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 ) ) )
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: ( ( 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) )

proof

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

proof

assume x in Y ; :: thesis: ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X )
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: ( x = f . i & f in X )
thus ( x = f . i & f in X ) by A4, A5; :: thesis: verum

end;

thus ( ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) implies x in Y ) by A3, CARD_3:def 6; :: thesis: verum

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: verum

proof

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: Y = pi (X,i)
thus Y c= pi (X,i) :: according to XBOOLE_0:def 10 :: thesis: pi (X,i) c= Y

proof

let y1 be object ; :: according to TARSKI:def 3 :: thesis: ( not y1 in Y or y1 in pi (X,i) )
assume y1 in Y ; :: thesis: y1 in pi (X,i)
then ex Eq being Equivalence_Relation of M st
( y1 = Eq . i & Eq in X ) by A6;
hence y1 in pi (X,i) by CARD_3:def 6; :: thesis: verum

end;

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

proof

let y1 be object ; :: according to TARSKI:def 3 :: thesis: ( not y1 in pi (X,i) or y1 in Y )
assume y1 in pi (X,i) ; :: thesis: y1 in Y
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 )

proof

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

end;

hence y1 in Y by A6; :: thesis: verum

end;

end;

end;