let X be RealUnitarySpace; :: thesis: for M being Subset of X holds Ort_CompSet M = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
let M be Subset of X; :: thesis: Ort_CompSet M = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
for z being object holds
( z in Ort_CompSet M iff z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } )

proof

let z be object ; :: thesis: ( z in Ort_CompSet M iff z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } )

hereby :: thesis: ( z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } implies z in Ort_CompSet M )

assume A1: z in Ort_CompSet M ; :: thesis: z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
then reconsider x = z as Point of X ;
for w being VECTOR of X st w in M holds
w,x are_orthogonal by Def1, A1;
hence z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } ; :: thesis: verum

end;

assume z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } ; :: thesis: z in Ort_CompSet M
then consider v being VECTOR of X such that
A2: ( z = v & ( for w being VECTOR of X st w in M holds
w,v are_orthogonal ) ) ;
for w being VECTOR of X st w in M holds
w .|. v = 0

proof

let w be VECTOR of X; :: thesis: ( w in M implies w .|. v = 0 )
assume w in M ; :: thesis: w .|. v = 0
then w,v are_orthogonal by A2;
hence w .|. v = 0 ; :: thesis: verum

end;

hence z in Ort_CompSet M by A2, Def1; :: thesis: verum

end;

hence Ort_CompSet M = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by TARSKI:2; :: thesis: verum