let X, x be set ; :: thesis: ( x in Dependencies X iff ex a, b being Subset of X st x = [a,b] )

hereby :: thesis: ( ex a, b being Subset of X st x = [a,b] implies x in Dependencies X )

assume A1: x in Dependencies X ; :: thesis: ex a, b being Subset of X st x = [a,b]
then consider a, b being set 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:106;
take a = a; :: thesis: ex b being Subset of X st x = [a,b]
take b = b; :: thesis: x = [a,b]
thus x = [a,b] by A2; :: thesis: verum

end;

given a, b being Subset of X such that A3: x = [a,b] ; :: thesis: x in Dependencies X
thus x in Dependencies X by A3, ZFMISC_1:106; :: thesis: verum