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

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