let V be RealUnitarySpace; :: thesis: for W being strict Subspace of V holds W /\ W = W
let W be strict Subspace of V; :: thesis: W /\ W = W
the carrier of W = the carrier of W /\ the carrier of W ;
hence W /\ W = W by Def2; :: thesis: verum