set X = product (Carrier J);
reconsider A = product_prebasis J as Subset-Family of (product (Carrier J)) ;
consider T being strict TopStruct such that
A1: T = TopStruct(# (product (Carrier J)),(UniCl (FinMeetCl A)) #) ;
reconsider T = T as strict TopSpace by A1, Th3;
take T ; :: thesis: ( the carrier of T = product (Carrier J) & product_prebasis J is prebasis of T )
thus the carrier of T = product (Carrier J) by A1; :: thesis: product_prebasis J is prebasis of T

now :: thesis: not {} in rng (Carrier J)

assume {} in rng (Carrier J) ; :: thesis: contradiction
then consider i being object such that
A2: i in dom (Carrier J) and
A3: {} = (Carrier J) . i by FUNCT_1:def 3;
consider R being 1-sorted such that
A4: R = J . i and
A5: {} = the carrier of R by A2, A3, PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A2, A4, FUNCT_1:def 3;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A5;
hence contradiction ; :: thesis: verum

end;

then not product (Carrier J) is empty by CARD_3:26;
hence product_prebasis J is prebasis of T by A1, CANTOR_1:18; :: thesis: verum