let F1, F2 be Subset-Family of X; :: thesis: ( ( for x being Subset of X holds
( x in F1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds
( x in F2 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) implies F1 = F2 )
assume that
A1: for x being Subset of X holds
( x in F1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) and
A2: for x being Subset of X holds
( x in F2 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ; :: thesis: F1 = F2

now :: thesis: for x being Subset of X holds
( x in F1 iff x in F2 )

let x be Subset of X; :: thesis: ( x in F1 iff x in F2 )
( x in F1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) by A1;
hence ( x in F1 iff x in F2 ) by A2; :: thesis: verum

end;

hence F1 = F2 by SUBSET_1:3; :: thesis: verum