let it1, it2 be Full-family of X; :: thesis: ( F c= it1 & ( for G being Dependency-set of X st F c= G & G is full_family holds
it1 c= G ) & F c= it2 & ( for G being Dependency-set of X st F c= G & G is full_family holds
it2 c= G ) implies it1 = it2 )
assume that
A2: F c= it1 and
A3: for G being Dependency-set of X st F c= G & G is full_family holds
it1 c= G and
A4: F c= it2 and
A5: for G being Dependency-set of X st F c= G & G is full_family holds
it2 c= G ; :: thesis: it1 = it2
A6: it2 c= it1 by A2, A5;
it1 c= it2 by A3, A4;
hence it1 = it2 by A6, XBOOLE_0:def 10; :: thesis: verum