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

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

a _|_

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

a _|_

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

set 0V = 0. S;

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

then - (- b) _|_ by RLVECT_1:17;

then A1: (0. S) - (- b) _|_ by RLVECT_1:4;

(- b) - a _|_ by Th1;

then a - (0. S) _|_ by A1, Def1;

then a _|_ by VECTSP_1:18;

then a _|_ by Def1;

then a _|_ by VECTSP_1:14;

hence a _|_ by RLVECT_1:17; :: thesis: verum

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

a _|_

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

a _|_

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

set 0V = 0. S;

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

then - (- b) _|_ by RLVECT_1:17;

then A1: (0. S) - (- b) _|_ by RLVECT_1:4;

(- b) - a _|_ by Th1;

then a - (0. S) _|_ by A1, Def1;

then a _|_ by VECTSP_1:18;

then a _|_ by Def1;

then a _|_ by VECTSP_1:14;

hence a _|_ by RLVECT_1:17; :: thesis: verum