let B1, B2 be Subset-Family of X; :: thesis: ( ( for x being Subset of X holds
( x in B1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of X holds
( x in B2 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ) implies B1 = B2 )
assume that
A1: for x being Subset of X holds
( x in B1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) and
A2: for x being Subset of X holds
( x in B2 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ; :: thesis: B1 = B2
now :: thesis: for x being Subset of X holds
( x in B2 iff x in B1 )
let x be Subset of X; :: thesis: ( x in B2 iff x in B1 )
( x in B2 iff ex Y being Subset-Family of X 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:3; :: thesis: verum