let T be TopStruct ; :: thesis: for A being Subset of
for t being Point of st t in A holds
Component_of t,A c= A
let A be Subset of ; :: thesis: for t being Point of st t in A holds
Component_of t,A c= A
let t be Point of ; :: 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:29;
hence Component_of t,A c= A by A2; :: thesis: verum