let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V st v <> 0. V & v in W holds
not v in Ort_Comp W
let W be Subspace of V; :: thesis: for v being VECTOR of V st v <> 0. V & v in W holds
not v in Ort_Comp W
let v be VECTOR of V; :: thesis: ( v <> 0. V & v in W implies not v in Ort_Comp W )
assume A1: v <> 0. V ; :: thesis: ( not v in W or not v in Ort_Comp W )
( v in W implies not v in Ort_Comp W )

proof

assume A2: v in W ; :: thesis: not v in Ort_Comp W
assume v in Ort_Comp W ; :: thesis: contradiction
then v in the carrier of (Ort_Comp W) ;
then v in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds
w,v1 are_orthogonal } by Def3;
then ex v1 being VECTOR of V st
( v = v1 & ( for w being VECTOR of V st w in W holds
w,v1 are_orthogonal ) ) ;
then v,v are_orthogonal by A2;
then 0 = v .|. v by BHSP_1:def 3;
hence contradiction by A1, BHSP_1:def 2; :: thesis: verum

end;

hence ( not v in W or not v in Ort_Comp W ) ; :: thesis: verum