[STATEMENT]
lemma subspace_S: "subspace S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subspace S
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
independent B
span B = S

goal (1 subgoal):
 1. subspace S
[PROOF STEP]
by auto