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

hereby :: thesis: ( ex N being non empty Subset of X st
( N = the carrier of M & H = Ort_Comp N ) implies H = Ort_Comp M )

assume A1: H = Ort_Comp M ; :: thesis: ex N being non empty Subset of X st
( N = the carrier of M & H = Ort_Comp N )
reconsider N = the carrier of M as non empty Subset of X by RUSUB_1:def 1;
take N = N; :: thesis: ( N = the carrier of M & H = Ort_Comp N )
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 3, A1
.= Ort_CompSet N by Lm4
.= { v where v is VECTOR of X : for w being VECTOR of X st w in N holds
w,v are_orthogonal } by Lm3 ;
hence ( N = the carrier of M & H = Ort_Comp N ) by RUSUB_5:def 4; :: thesis: verum

end;

given N being non empty Subset of X such that A2: ( N = the carrier of M & H = Ort_Comp N ) ; :: thesis: H = Ort_Comp M
the carrier of H = { v where v is VECTOR of X : for w being VECTOR of X st w in N holds
w,v are_orthogonal } by A2, RUSUB_5:def 4
.= Ort_CompSet N by Lm3
.= { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by Lm4, A2 ;
hence H = Ort_Comp M by RUSUB_5:def 3; :: thesis: verum