let V be RealLinearSpace; :: thesis: for A, B being Subset of V st Z_Lin A = Z_Lin B holds
Lin A = Lin B
let A, B be Subset of V; :: thesis: ( Z_Lin A = Z_Lin B implies Lin A = Lin B )
assume Z_Lin A = Z_Lin B ; :: thesis: Lin A = Lin B
hence Lin A = Lin (Z_Lin B) by Th34
.= Lin B by Th34 ;
:: thesis: verum