let P1, P2 be Subset-Family of (product (Carrier J)); :: thesis: ( ( for x being Subset of (product (Carrier J)) holds
( x in P1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) ) & ( for x being Subset of (product (Carrier J)) holds
( x in P2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) ) implies P1 = P2 )
assume that
A1: for x being Subset of (product (Carrier J)) holds
( x in P1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) and
A2: for x being Subset of (product (Carrier J)) holds
( x in P2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) ; :: thesis: P1 = P2
A3: P1 c= P2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 or x in P2 )
assume A4: x in P1 ; :: thesis: x in P2
then reconsider x' = x as Subset of (product (Carrier J)) ;
ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x' = product ((Carrier J) +* i,V) ) by A1, A4;
hence x in P2 by A2; :: thesis: verum

end;

P2 c= P1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P2 or x in P1 )
assume A5: x in P2 ; :: thesis: x in P1
then reconsider x' = x as Subset of (product (Carrier J)) ;
ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x' = product ((Carrier J) +* i,V) ) by A2, A5;
hence x in P1 by A1; :: thesis: verum

end;

hence P1 = P2 by A3, XBOOLE_0:def 10; :: thesis: verum