let T be TopStruct ; :: thesis: for A being Subset of T
for t being Point of T st t in A holds
Component_of (t,A) c= A
let A be Subset of T; :: thesis: for t being Point of T st t in A holds
Component_of (t,A) c= A
let t be Point of T; :: thesis: ( t in A implies Component_of (t,A) c= A )
assume A1: t in A ; :: thesis: Component_of (t,A) c= A
then Down (t,A) = t by CONNSP_3:def 3;
then A2: Component_of (t,A) = Component_of (Down (t,A)) by A1, CONNSP_3:def 7;
the carrier of (T | A) = A by PRE_TOPC:8;
hence Component_of (t,A) c= A by A2; :: thesis: verum