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 ) )

( 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

( 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 )

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 )

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;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

( 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