let X, x be set ; 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; ( x in M implies ex a, b being Subset of X st x = [a,b] )
assume A1:
x in M
; 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
; ex b being Subset of X st x = [a,b]
take
b
; x = [a,b]
thus
x = [a,b]
by A2; verum