let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for G being Subset of () st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] () c= union G

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I
for xi being Element of (J . i)
for G being Subset of () st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] () c= union G

let i be Element of I; :: thesis: for xi being Element of (J . i)
for G being Subset of () st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] () c= union G

let xi be Element of (J . i); :: thesis: for G being Subset of () st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] () c= union G

let G be Subset of (); :: thesis: ( (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) implies [#] () c= union G )

assume that
A1: (proj (J,i)) " {xi} c= union G and
A2: for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ; :: thesis: [#] () c= union G
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in [#] () or f in union G )
assume f in [#] () ; :: thesis: f in union G
then reconsider f9 = f as Element of () ;
set g = f9 +* (i,xi);
A3: f9 +* (i,xi) in (proj (J,i)) " {xi} by Th11;
then consider Ag being set such that
A4: f9 +* (i,xi) in Ag and
A5: Ag in G by ;
consider i2 being Element of I, Ai2 being Subset of (J . i2) such that
Ai2 is open and
A6: (proj (J,i2)) " Ai2 = Ag by ;
A7: Ai2 <> [#] (J . i2)
proof
assume Ai2 = [#] (J . i2) ; :: thesis: contradiction
then (proj (J,i2)) " Ai2 = [#] () by Th10
.= the carrier of () ;
hence contradiction by A2, A5, A6; :: thesis: verum
end;
A8: not (proj (J,i)) " {xi} c= (proj (J,i2)) " Ai2 by A2, A5, A6;
i <> i2
proof
assume A9: i = i2 ; :: thesis: contradiction
then reconsider Ai29 = Ai2 as Subset of (J . i) ;
((proj (J,i)) " {xi}) /\ ((proj (J,i)) " Ai29) <> {} by ;
then A10: (proj (J,i)) " {xi} meets (proj (J,i)) " Ai29 ;
not xi in Ai2 by A8, A7, A9, Th12;
hence contradiction by A10, Th9; :: thesis: verum
end;
then f in (proj (J,i2)) " Ai2 by A4, A6, Th13;
hence f in union G by ; :: thesis: verum