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 A2: 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
A3: ( f in X & x = f . i ) by A2, CARD_3:def 6;
reconsider f = f as Equivalence_Relation of M by A3, MSUALG_5:def 5;
take f ; :: thesis: ( x = f . i & f in X )
thus ( x = f . i & f in X ) by A3; :: thesis: verum

end;

thus ( ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) implies x in Y ) by A2, 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 A4: 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 set ; :: 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 consider Eq being Equivalence_Relation of M such that
A5: ( y1 = Eq . i & Eq in X ) by A4;
thus y1 in pi X,i by A5, CARD_3:def 6; :: thesis: verum

end;

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

proof

let y1 be set ; :: 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
A6: ( f in X & y1 = f . i ) by CARD_3:def 6;
reconsider f = f as Equivalence_Relation of M by A6, 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 A6; :: thesis: verum

end;

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

end;

end;

end;