theorem Th12: :: YELLOW17:12

for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )