let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj J,i) " {xi} meets (proj J,i) " Ai holds
xi in Ai
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj J,i) " {xi} meets (proj J,i) " Ai holds
xi in Ai
let i be Element of I; :: thesis: for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj J,i) " {xi} meets (proj J,i) " Ai holds
xi in Ai
let xi be Element of (J . i); :: thesis: for Ai being Subset of (J . i) st (proj J,i) " {xi} meets (proj J,i) " Ai holds
xi in Ai
let Ai be Subset of (J . i); :: thesis: ( (proj J,i) " {xi} meets (proj J,i) " Ai implies xi in Ai )
assume ((proj J,i) " {xi}) /\ ((proj J,i) " Ai) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: xi in Ai
then ((proj (Carrier J),i) " {xi}) /\ ((proj J,i) " Ai) <> {} by WAYBEL18:def 4;
then ((proj (Carrier J),i) " {xi}) /\ ((proj (Carrier J),i) " Ai) <> {} by WAYBEL18:def 4;
then A1: (proj (Carrier J),i) " {xi} meets (proj (Carrier J),i) " Ai by XBOOLE_0:def 7;
Ai c= the carrier of (J . i) ;
then Ai c= (Carrier J) . i by YELLOW_6:9;
hence xi in Ai by A1, Th1; :: thesis: verum