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 ( 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 ) ) ; :: thesis: it1 = it2
then ( it1 c= it2 & it2 c= it1 ) ;
hence it1 = it2 by XBOOLE_0:def 10; :: thesis: verum