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

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

d _|_

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

d _|_

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

assume that

A1: d _|_ and

A2: d _|_ ; :: thesis: d _|_

d _|_ by A1, Th6;

then d _|_ by VECTSP_1:17;

then d _|_ by A2, Def1;

then d _|_ by RLVECT_1:def 3;

then d _|_ by RLVECT_1:def 3;

then d _|_ by RLVECT_1:5;

hence d _|_ by RLVECT_1:4; :: thesis: verum

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

d _|_

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

d _|_

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

assume that

A1: d _|_ and

A2: d _|_ ; :: thesis: d _|_

d _|_ by A1, Th6;

then d _|_ by VECTSP_1:17;

then d _|_ by A2, Def1;

then d _|_ by RLVECT_1:def 3;

then d _|_ by RLVECT_1:def 3;

then d _|_ by RLVECT_1:5;

hence d _|_ by RLVECT_1:4; :: thesis: verum