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

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

not a _|_

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

not a _|_

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

assume that

A1: not a _|_ and

A2: a _|_ ; :: thesis: not a _|_

a _|_ by A2, Def1;

then A3: a _|_ by VECTSP_1:14;

assume a _|_ ; :: thesis: contradiction

then a _|_ by A3, Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

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

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

not a _|_

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

not a _|_

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

assume that

A1: not a _|_ and

A2: a _|_ ; :: thesis: not a _|_

a _|_ by A2, Def1;

then A3: a _|_ by VECTSP_1:14;

assume a _|_ ; :: thesis: contradiction

then a _|_ by A3, Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

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