let A1, A2 be Subset-Family of X; :: thesis: ( ( for x being object holds
( x in A1 iff ex S being Subset of X st
( S = x & S is f -closed ) ) ) & ( for x being object holds
( x in A2 iff ex S being Subset of X st
( S = x & S is f -closed ) ) ) implies A1 = A2 )
assume that
A1: for x being object holds
( x in A1 iff ex S being Subset of X st
( S = x & S is f -closed ) ) and
A2: for x being object holds
( x in A2 iff ex S being Subset of X st
( S = x & S is f -closed ) ) ; :: thesis: A1 = A2
defpred S₁[ object ] means ex S being Subset of X st
( S = $1 & S is f -closed );
A3: for x being object holds
( x in A1 iff S₁[x] ) by A1;
A4: for x being object holds
( x in A2 iff S₁[x] ) by A2;
A1 = A2 from XBOOLE_0:sch 2(A3, A4);
hence A1 = A2 ; :: thesis: verum