let V be RealLinearSpace; :: thesis: for A, B being Subset of V st A c= B holds
Z_Lin A c= Z_Lin B
let A, B be Subset of V; :: thesis: ( A c= B implies Z_Lin A c= Z_Lin B )
assume A1: A c= B ; :: thesis: Z_Lin A c= Z_Lin B
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in Z_Lin A or v in Z_Lin B )
assume v in Z_Lin A ; :: thesis: v in Z_Lin B
then consider l being Linear_Combination of A such that
A2: ( v = Sum l & rng l c= INT ) ;
reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21;
Sum l = v by A2;
hence v in Z_Lin B by A2; :: thesis: verum