let B1, B2 be Subset-Family of ; :: thesis: ( ( for x being Subset of holds
( x in B1 iff ex Y being Subset-Family of st
( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of holds
( x in B2 iff ex Y being Subset-Family of st
( Y c= A & Y is finite & x = Intersect Y ) ) ) implies B1 = B2 )
assume that
A1: for x being Subset of holds
( x in B1 iff ex Y being Subset-Family of st
( Y c= A & Y is finite & x = Intersect Y ) ) and
A2: for x being Subset of holds
( x in B2 iff ex Y being Subset-Family of st
( Y c= A & Y is finite & x = Intersect Y ) ) ; :: thesis: B1 = B2

now

let x be Subset of ; :: thesis: ( x in B2 iff x in B1 )
( x in B2 iff ex Y being Subset-Family of st
( Y c= A & Y is finite & x = Intersect Y ) ) by A2;
hence ( x in B2 iff x in B1 ) by A1; :: thesis: verum

end;

hence B1 = B2 by SUBSET_1:8; :: thesis: verum