let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds
not v in W
let W be Subspace of V; :: thesis: for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds
not v in W
let v be VECTOR of V; :: thesis: ( v <> 0. V & v in Ort_Comp W implies not v in W )
assume A1: v <> 0. V ; :: thesis: ( not v in Ort_Comp W or not v in W )
( v in Ort_Comp W implies not v in W )
proof
assume A2: v in Ort_Comp W ; :: thesis: not v in W
assume A3: v in W ; :: thesis: contradiction
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 A2, RUSUB_5:def 3;
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 A3;
hence contradiction by A1, BHSP_1:def 2; :: thesis: verum
end;
hence ( not v in Ort_Comp W or not v in W ) ; :: thesis: verum