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

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

now

let y be set ; :: thesis: ( y in A1 iff y in A2 )
( y in A1 iff y is_upper_min_depend_of G ) by A26;
hence ( y in A1 iff y in A2 ) by A27; :: thesis: verum

end;

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