let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
let u, v be VECTOR of V; :: thesis: for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
let W be Subspace of V; :: thesis: ( u in v + W & u in (- v) + W implies v in W )
assume ( u in v + W & u in (- v) + W ) ; :: thesis: v in W
then v + W = (- v) + W by Th72;
hence v in W by Th71; :: thesis: verum