defpred S1[ object ] means ex W being Subset of T st
( $1 = Der W & W in F );
let H, G be Subset-Family of T; :: thesis: ( ( for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Der B & B in F ) ) ) & ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Der B & B in F ) ) ) implies H = G )
assume that
A1: for Z being Subset of T holds
( Z in H iff S1[Z] ) and
A2: for X being Subset of T holds
( X in G iff S1[X] ) ; :: thesis: H = G
now :: thesis: for X being object st X in G holds
X in H
let X be object ; :: thesis: ( X in G implies X in H )
assume A3: X in G ; :: thesis: X in H
then reconsider X9 = X as Subset of T ;
S1[X9] by A2, A3;
hence X in H by A1; :: thesis: verum
end;
then A4: G c= H ;
now :: thesis: for Z being object st Z in H holds
Z in G
let Z be object ; :: thesis: ( Z in H implies Z in G )
assume Z in H ; :: thesis: Z in G
then S1[Z] by A1;
hence Z in G by A2; :: thesis: verum
end;
then H c= G ;
hence H = G by A4; :: thesis: verum