let X, x be set ; :: thesis: for F being Dependency-set of X st x in F holds
ex a, b being Subset of X st x = [a,b]
let M be Dependency-set of X; :: thesis: ( x in M implies ex a, b being Subset of X st x = [a,b] )
assume A1: x in M ; :: thesis: ex a, b being Subset of X st x = [a,b]
then consider a, b being object such that
A2: [a,b] = x by RELAT_1:def 1;
reconsider a = a, b = b as Subset of X by A1, A2, ZFMISC_1:87;
take a ; :: thesis: ex b being Subset of X st x = [a,b]
take b ; :: thesis: x = [a,b]
thus x = [a,b] by A2; :: thesis: verum