let A1, A2 be a_partition of Y; :: thesis: ( ( G <> {} & ( for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 ) & ( not G <> {} & A1 = %I Y & A2 = %I Y implies A1 = A2 ) )

now :: thesis: ( G <> {} & ( for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 )

assume that
G <> {} and
A26: for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) and
A27: for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ; :: thesis: A1 = A2
for y being object holds
( y in A1 iff y in A2 ) by A27, A26;
hence A1 = A2 by TARSKI:2; :: thesis: verum

end;

hence ( ( G <> {} & ( for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 ) & ( not G <> {} & A1 = %I Y & A2 = %I Y implies A1 = A2 ) ) ; :: thesis: verum