let X, x be set ; ( x in Dependencies X iff ex a, b being Subset of X st x = [a,b] )
hereby ( ex a, b being Subset of X st x = [a,b] implies x in Dependencies X )
assume A1:
x in Dependencies X
;
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 =
a;
ex b being Subset of X st x = [a,b]take b =
b;
x = [a,b]thus
x = [a,b]
by A2;
verum
end;
given a, b being Subset of X such that A3:
x = [a,b]
; x in Dependencies X
thus
x in Dependencies X
by A3, ZFMISC_1:87; verum