let X be RealUnitarySpace; :: thesis: for M being non empty Subset of X
for H being strict Subspace of X holds
( H = Ort_Comp M iff the carrier of H = Ort_CompSet M )
let M be non empty Subset of X; :: thesis: for H being strict Subspace of X holds
( H = Ort_Comp M iff the carrier of H = Ort_CompSet M )
let H be strict Subspace of X; :: thesis: ( H = Ort_Comp M iff the carrier of H = Ort_CompSet M )

hereby :: thesis: ( the carrier of H = Ort_CompSet M implies H = Ort_Comp M )

assume H = Ort_Comp M ; :: thesis: the carrier of H = Ort_CompSet M
hence the carrier of H = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by RUSUB_5:def 4
.= Ort_CompSet M by Lm3 ;
:: thesis: verum

end;

assume the carrier of H = Ort_CompSet M ; :: thesis: H = Ort_Comp M
then the carrier of H = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by Lm3;
hence H = Ort_Comp M by RUSUB_5:def 4; :: thesis: verum