let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I holds the topology of (product J) = product_prebasis J

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: the topology of (product J) = product_prebasis J

reconsider T = product J as TopSpace ;

reconsider K = product_prebasis J as Subset-Family of T by WAYBEL18:def 3;

K is prebasis of T by WAYBEL18:def 3;

then A1: UniCl (FinMeetCl K) = the topology of T by YELLOW_9:22, YELLOW_9:23;

FinMeetCl K = FinMeetCl (product_prebasis J) by WAYBEL18:def 3;

then UniCl (FinMeetCl K) = UniCl (FinMeetCl (product_prebasis J)) by WAYBEL18:def 3;

hence the topology of (product J) = product_prebasis J by A1, Lm7; :: thesis: verum

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: the topology of (product J) = product_prebasis J

reconsider T = product J as TopSpace ;

reconsider K = product_prebasis J as Subset-Family of T by WAYBEL18:def 3;

K is prebasis of T by WAYBEL18:def 3;

then A1: UniCl (FinMeetCl K) = the topology of T by YELLOW_9:22, YELLOW_9:23;

FinMeetCl K = FinMeetCl (product_prebasis J) by WAYBEL18:def 3;

then UniCl (FinMeetCl K) = UniCl (FinMeetCl (product_prebasis J)) by WAYBEL18:def 3;

hence the topology of (product J) = product_prebasis J by A1, Lm7; :: thesis: verum