let S be Subset of (NLin (rng x)); :: thesis: ( S <> {} & S is open implies D meets S )
assume A2: ( S <> {} & S is open ) ; :: thesis: D meets S
consider z being object such that
A3: z in S by A2, XBOOLE_0:def 1;
reconsider z = z as Point of (NLin (rng x)) by A3;
consider e being Real such that
A4: ( 0 < e & { y where y is Point of (NLin (rng x)) : ||.(y - z).|| < e } c= S ) by A2, A3, NDIFF_1:3;
z in Lin (rng x) ;
then consider l being Linear_Combination of rng x such that
A5: z = Sum l by RLVECT_3:14;
consider m being Linear_Combination of rng x such that
A6: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) by A4, Th23;
Sum m in Lin (rng x) by RLVECT_3:14;
then reconsider y = Sum m as Point of (NLin (rng x)) ;
- (Sum m) = (- 1) * (Sum m) by RLVECT_1:16
.= (- 1) * y by NORMSP_3:28
.= - y by RLVECT_1:16 ;
then (Sum l) - (Sum m) = z - y by A5, NORMSP_3:28;
then ||.((Sum l) - (Sum m)).|| = ||.(z - y).|| by NORMSP_3:28;
then ||.(y - z).|| < e by A6, NORMSP_1:7;
then A8: y in { v where v is Point of (NLin (rng x)) : ||.(v - z).|| < e } ;
y in D by A1, A6;
hence D meets S by A4, A8, XBOOLE_0:def 4; :: thesis: verum