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 _|_
proof
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;
ex c being Element of S st
( not a _|_ & not a _|_ & not a _|_ & not a _|_ ) by A3, Def1;
hence contradiction by A5; :: thesis: verum