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

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

not b _|_

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

not b _|_

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

assume that

A1: not b _|_ and

A2: b _|_ ; :: thesis: not b _|_

assume b _|_ ; :: thesis: contradiction

then b _|_ by Def1;

then b _|_ by VECTSP_1:14;

then b _|_ by A2, Def1;

then b _|_ by RLVECT_1:def 3;

then b _|_ by RLVECT_1:5;

hence contradiction by A1, RLVECT_1:4; :: thesis: verum

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

not b _|_

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

not b _|_

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

assume that

A1: not b _|_ and

A2: b _|_ ; :: thesis: not b _|_

assume b _|_ ; :: thesis: contradiction

then b _|_ by Def1;

then b _|_ by VECTSP_1:14;

then b _|_ by A2, Def1;

then b _|_ by RLVECT_1:def 3;

then b _|_ by RLVECT_1:5;

hence contradiction by A1, RLVECT_1:4; :: thesis: verum