let F be Field; :: thesis: for S being OrtSp of F st (1_ F) + (1_ F) <> 0. F & ex a being Element of S st a <> 0. S holds

ex b being Element of S st not b _|_

let S be OrtSp of F; :: thesis: ( (1_ F) + (1_ F) <> 0. F & ex a being Element of S st a <> 0. S implies ex b being Element of S st not b _|_ )

set 1F = 1_ F;

set 0V = 0. S;

assume that

A1: (1_ F) + (1_ F) <> 0. F and

A2: ex a being Element of S st a <> 0. S ; :: thesis: not for b being Element of S holds b _|_

consider a being Element of S such that

A3: a <> 0. S by A2;

assume A4: for b being Element of S holds b _|_ ; :: thesis: contradiction

A5: for c, d being Element of S holds d _|_

( not a _|_ & not a _|_ & not a _|_ & not a _|_ ) by A3, Def1;

hence contradiction by A5; :: thesis: verum

ex b being Element of S st not b _|_

let S be OrtSp of F; :: thesis: ( (1_ F) + (1_ F) <> 0. F & ex a being Element of S st a <> 0. S implies ex b being Element of S st not b _|_ )

set 1F = 1_ F;

set 0V = 0. S;

assume that

A1: (1_ F) + (1_ F) <> 0. F and

A2: ex a being Element of S st a <> 0. S ; :: thesis: not for b being Element of S holds b _|_

consider a being Element of S such that

A3: a <> 0. S by A2;

assume A4: for b being Element of S holds b _|_ ; :: thesis: contradiction

A5: for c, d being Element of S holds d _|_

proof

ex c being Element of S st
let c, d be Element of S; :: thesis: d _|_

( d _|_ & c _|_ ) by A4;

then d - c _|_ by Th9;

then A6: d + c _|_ by Th2;

d + c _|_ by A4;

then d + c _|_ by A6, Def1;

then d + c _|_ by RLVECT_1:def 3;

then d + c _|_ by RLVECT_1:def 3;

then d + c _|_ by RLVECT_1:5;

then d + c _|_ by RLVECT_1:4;

then d + c _|_ by VECTSP_1:def 17;

then d + c _|_ by VECTSP_1:def 17;

then d + c _|_ by VECTSP_1:def 15;

then d + c _|_ by Def1;

then d + c _|_ by VECTSP_1:def 16;

then d + c _|_ by A1, VECTSP_1:def 10;

then d + c _|_ by VECTSP_1:def 17;

then A7: d _|_ by Th2;

d _|_ by A4, Th6;

then d _|_ by A7, Def1;

then d _|_ by RLVECT_1:def 3;

then d _|_ by RLVECT_1:5;

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

end;( d _|_ & c _|_ ) by A4;

then d - c _|_ by Th9;

then A6: d + c _|_ by Th2;

d + c _|_ by A4;

then d + c _|_ by A6, Def1;

then d + c _|_ by RLVECT_1:def 3;

then d + c _|_ by RLVECT_1:def 3;

then d + c _|_ by RLVECT_1:5;

then d + c _|_ by RLVECT_1:4;

then d + c _|_ by VECTSP_1:def 17;

then d + c _|_ by VECTSP_1:def 17;

then d + c _|_ by VECTSP_1:def 15;

then d + c _|_ by Def1;

then d + c _|_ by VECTSP_1:def 16;

then d + c _|_ by A1, VECTSP_1:def 10;

then d + c _|_ by VECTSP_1:def 17;

then A7: d _|_ by Th2;

d _|_ by A4, Th6;

then d _|_ by A7, Def1;

then d _|_ by RLVECT_1:def 3;

then d _|_ by RLVECT_1:5;

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

( not a _|_ & not a _|_ & not a _|_ & not a _|_ ) by A3, Def1;

hence contradiction by A5; :: thesis: verum