let X, A be set ; :: thesis: for F being Dependency-set of X st A in charact_set F holds
( A is Subset of X & ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) )
let F be Dependency-set of X; :: thesis: ( A in charact_set F implies ( A is Subset of X & ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) ) )
assume A in charact_set F ; :: thesis: ( A is Subset of X & ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) )
then ex Y being Subset of X st
( A = Y & ex a, b being Subset of X st
( [a,b] in F & a c= Y & not b c= Y ) ) ;
hence ( A is Subset of X & ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) ) ; :: thesis: verum