let F be Field; :: thesis: for S being OrtSp of F

for a, b being Element of S st b _|_ holds

b _|_

let S be OrtSp of F; :: thesis: for a, b being Element of S st b _|_ holds

b _|_

let a, b be Element of S; :: thesis: ( b _|_ implies b _|_ )

assume b _|_ ; :: thesis: b _|_

then b _|_ by Def1;

hence b _|_ by VECTSP_1:14; :: thesis: verum

for a, b being Element of S st b _|_ holds

b _|_

let S be OrtSp of F; :: thesis: for a, b being Element of S st b _|_ holds

b _|_

let a, b be Element of S; :: thesis: ( b _|_ implies b _|_ )

assume b _|_ ; :: thesis: b _|_

then b _|_ by Def1;

hence b _|_ by VECTSP_1:14; :: thesis: verum