let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for u, v being VECTOR of V st u in v + W & u in (- v) + W holds
v in W
let W be Subspace of V; :: thesis: for u, v being VECTOR of V st u in v + W & u in (- v) + W holds
v in W
let u, v be VECTOR 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 Th50;
hence v in W by Th49; :: thesis: verum