let X be RealUnitarySpace; :: thesis: for M being Subset of X holds Ort_CompSet M is linearly-closed
let M be Subset of X; :: thesis: Ort_CompSet M is linearly-closed
A1: for v, u being VECTOR of X st v in Ort_CompSet M & u in Ort_CompSet M holds
v + u in Ort_CompSet M

proof

let v, u be VECTOR of X; :: thesis: ( v in Ort_CompSet M & u in Ort_CompSet M implies v + u in Ort_CompSet M )
assume A2: ( v in Ort_CompSet M & u in Ort_CompSet M ) ; :: thesis: v + u in Ort_CompSet M

now :: thesis: for x being Point of X st x in M holds
x .|. (u + v) = 0

let x be Point of X; :: thesis: ( x in M implies x .|. (u + v) = 0 )
assume x in M ; :: thesis: x .|. (u + v) = 0
then A3: ( x .|. v = 0 & x .|. u = 0 ) by A2, Def1;
thus x .|. (u + v) = (x .|. u) + (x .|. v) by BHSP_1:2
.= 0 by A3 ; :: thesis: verum

end;

hence v + u in Ort_CompSet M by Def1; :: thesis: verum

end;

for a being Real
for v being VECTOR of X st v in Ort_CompSet M holds
a * v in Ort_CompSet M

proof

let a be Real; :: thesis: for v being VECTOR of X st v in Ort_CompSet M holds
a * v in Ort_CompSet M
let u be VECTOR of X; :: thesis: ( u in Ort_CompSet M implies a * u in Ort_CompSet M )
assume A4: u in Ort_CompSet M ; :: thesis: a * u in Ort_CompSet M

now :: thesis: for x being Point of X st x in M holds
x .|. (a * u) = 0

let x be Point of X; :: thesis: ( x in M implies x .|. (a * u) = 0 )
assume A5: x in M ; :: thesis: x .|. (a * u) = 0
thus x .|. (a * u) = a * (x .|. u) by BHSP_1:3
.= a * 0 by A5, A4, Def1
.= 0 ; :: thesis: verum

end;

hence a * u in Ort_CompSet M by Def1; :: thesis: verum

end;

hence Ort_CompSet M is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum