let A be set ; :: thesis: for X being non empty set

for S being a_partition of X st A in S holds

ex x being Element of X st A = EqClass (x,S)

let X be non empty set ; :: thesis: for S being a_partition of X st A in S holds

ex x being Element of X st A = EqClass (x,S)

let S be a_partition of X; :: thesis: ( A in S implies ex x being Element of X st A = EqClass (x,S) )

assume A1: A in S ; :: thesis: ex x being Element of X st A = EqClass (x,S)

then not A is empty by Def4;

then consider x being object such that

A2: x in A ;

take x ; :: thesis: ( x is set & x is Element of X & A = EqClass (x,S) )

thus ( x is set & x is Element of X & A = EqClass (x,S) ) by A1, A2, Def6; :: thesis: verum

for S being a_partition of X st A in S holds

ex x being Element of X st A = EqClass (x,S)

let X be non empty set ; :: thesis: for S being a_partition of X st A in S holds

ex x being Element of X st A = EqClass (x,S)

let S be a_partition of X; :: thesis: ( A in S implies ex x being Element of X st A = EqClass (x,S) )

assume A1: A in S ; :: thesis: ex x being Element of X st A = EqClass (x,S)

then not A is empty by Def4;

then consider x being object such that

A2: x in A ;

take x ; :: thesis: ( x is set & x is Element of X & A = EqClass (x,S) )

thus ( x is set & x is Element of X & A = EqClass (x,S) ) by A1, A2, Def6; :: thesis: verum