let F be Field; :: thesis: for S being OrtSp of F
for a, b being Element of S st b _|_ holds
a _|_
let S be OrtSp of F; :: thesis: for a, b being Element of S st b _|_ holds
a _|_
let a, b be Element of S; :: thesis: ( b _|_ implies a _|_ )
set 0V = 0. S;
assume b _|_ ; :: thesis: a _|_
then - (- b) _|_ by RLVECT_1:30;
then (0. S) + (- (- b)) _|_ by RLVECT_1:10;
then A1: (0. S) - (- b) _|_ ;
(- b) - a _|_ by Th11;
then a - (0. S) _|_ by A1, Def2;
then a _|_ by VECTSP_1:65;
then a _|_ by Def2;
then a _|_ by VECTSP_1:59;
hence a _|_ by RLVECT_1:30; :: thesis: verum