let X be non empty set ; 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; 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; 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 ; ( 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 }
; 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
; ( S in F & A = EqClass (x,S) )
thus
( S in F & A = EqClass (x,S) )
by A1; verum