let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds
B c= BDD A
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_inside_component_of A implies B c= BDD A )
assume B is_inside_component_of A ; :: thesis: B c= BDD A
then A1: B in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_inside_component_of A } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in BDD A )
assume x in B ; :: thesis: x in BDD A
hence x in BDD A by A1, TARSKI:def 4; :: thesis: verum