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 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 TopStruct-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 ((),i)) " {xi}) /\ ((proj (J,i)) " Ai) <> {} by WAYBEL18:def 4;
then ((proj ((),i)) " {xi}) /\ ((proj ((),i)) " Ai) <> {} by WAYBEL18:def 4;
then A1: (proj ((),i)) " {xi} meets (proj ((),i)) " Ai ;
Ai c= the carrier of (J . i) ;
then Ai c= () . i by YELLOW_6:2;
hence xi in Ai by ; :: thesis: verum