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: P2 c= P1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P2 or x in P1 )
assume A4: x in P2 ; :: thesis: x in P1
then reconsider x9 = 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 & x9 = product ((Carrier J) +* (i,V)) ) by A2, A4;
hence x in P1 by A1; :: thesis: verum
end;
P1 c= P2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 or x in P2 )
assume A5: x in P1 ; :: thesis: x in P2
then reconsider x9 = 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 & x9 = product ((Carrier J) +* (i,V)) ) by A1, A5;
hence x in P2 by A2; :: thesis: verum
end;
hence P1 = P2 by A3; :: thesis: verum