let X be non empty set ; :: thesis: for x being Element of X

for F being Part-Family of X

for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds

ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

let x be Element of X; :: thesis: for F being Part-Family of X

for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds

ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

let F be Part-Family of X; :: thesis: for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds

ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

let A be set ; :: thesis: ( A in { (EqClass (x,S)) where S is a_partition of X : S in F } implies ex T being a_partition of X st

( T in F & A = EqClass (x,T) ) )

assume A in { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

then consider S being a_partition of X such that

A1: ( A = EqClass (x,S) & S in F ) ;

take S ; :: thesis: ( S in F & A = EqClass (x,S) )

thus ( S in F & A = EqClass (x,S) ) by A1; :: thesis: verum

for F being Part-Family of X

for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds

ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

let x be Element of X; :: thesis: for F being Part-Family of X

for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds

ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

let F be Part-Family of X; :: thesis: for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds

ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

let A be set ; :: thesis: ( A in { (EqClass (x,S)) where S is a_partition of X : S in F } implies ex T being a_partition of X st

( T in F & A = EqClass (x,T) ) )

assume A in { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: ex T being a_partition of X st

( T in F & A = EqClass (x,T) )

then consider S being a_partition of X such that

A1: ( A = EqClass (x,S) & S in F ) ;

take S ; :: thesis: ( S in F & A = EqClass (x,S) )

thus ( S in F & A = EqClass (x,S) ) by A1; :: thesis: verum