let F be Function; :: thesis: for i, xi being set
for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds
xi in Ai
let i, xi be set ; :: thesis: for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds
xi in Ai
let Ai be Subset of (F . i); :: thesis: ( (proj (F,i)) " {xi} meets (proj (F,i)) " Ai implies xi in Ai )
set f = the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai);
assume A1: ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: xi in Ai
then the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) in (proj (F,i)) " {xi} by XBOOLE_0:def 4;
then (proj (F,i)) . the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) in {xi} by FUNCT_1:def 7;
then A2: (proj (F,i)) . the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) = xi by TARSKI:def 1;
the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) in (proj (F,i)) " Ai by A1, XBOOLE_0:def 4;
hence xi in Ai by A2, FUNCT_1:def 7; :: thesis: verum