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 ((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 ;
Ai c= the carrier of (J . i) ;
then Ai c= (Carrier J) . i by YELLOW_6:2;
hence xi in Ai by A1, Th1; :: thesis: verum