let X be RealUnitarySpace; :: thesis: for S, T being non empty Subset of X st S c= T holds
Ort_Comp T is Subspace of Ort_Comp S
let S, T be non empty Subset of X; :: thesis: ( S c= T implies Ort_Comp T is Subspace of Ort_Comp S )
assume A1: S c= T ; :: thesis: Ort_Comp T is Subspace of Ort_Comp S
A2: ( the carrier of (Ort_Comp S) = Ort_CompSet S & the carrier of (Ort_Comp T) = Ort_CompSet T ) by Lm5;
Ort_CompSet T c= Ort_CompSet S

proof

let x0 be object ; :: according to TARSKI:def 3 :: thesis: ( not x0 in Ort_CompSet T or x0 in Ort_CompSet S )
assume A3: x0 in Ort_CompSet T ; :: thesis: x0 in Ort_CompSet S
then reconsider x = x0 as Point of X ;
for y being Point of X st y in S holds
y .|. x = 0 by A1, A3, Def1;
hence x0 in Ort_CompSet S by Def1; :: thesis: verum

end;

hence Ort_Comp T is Subspace of Ort_Comp S by RUSUB_1:22, A2; :: thesis: verum