let X, A be set ; 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; ( 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
; ( 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 ) )
; verum