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

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

a - b _|_

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

a - b _|_

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

set 0V = 0. S;

assume that

A1: a _|_ and

A2: b _|_ ; :: thesis: a - b _|_

a _|_ by A1, Def1;

then a _|_ by VECTSP_1:14;

then - a _|_ by Th2;

then (0. S) + (- a) _|_ by RLVECT_1:4;

then (b + (- b)) + (- a) _|_ by RLVECT_1:5;

then b + ((- b) - a) _|_ by RLVECT_1:def 3;

then A3: b - (a + b) _|_ by VECTSP_1:17;

b + (0. S) _|_ by A2, RLVECT_1:4;

then b + (a + (- a)) _|_ by RLVECT_1:5;

then (a + b) - a _|_ by RLVECT_1:def 3;

hence a - b _|_ by A3, Def1; :: thesis: verum

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

a - b _|_

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

a - b _|_

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

set 0V = 0. S;

assume that

A1: a _|_ and

A2: b _|_ ; :: thesis: a - b _|_

a _|_ by A1, Def1;

then a _|_ by VECTSP_1:14;

then - a _|_ by Th2;

then (0. S) + (- a) _|_ by RLVECT_1:4;

then (b + (- b)) + (- a) _|_ by RLVECT_1:5;

then b + ((- b) - a) _|_ by RLVECT_1:def 3;

then A3: b - (a + b) _|_ by VECTSP_1:17;

b + (0. S) _|_ by A2, RLVECT_1:4;

then b + (a + (- a)) _|_ by RLVECT_1:5;

then (a + b) - a _|_ by RLVECT_1:def 3;

hence a - b _|_ by A3, Def1; :: thesis: verum