let F be Field; :: thesis: for S being OrtSp of F
for a, b, c, d being Element of S st d _|_ & d _|_ holds
d _|_
let S be OrtSp of F; :: thesis: for a, b, c, d being Element of S st d _|_ & d _|_ holds
d _|_
let a, b, c, d be Element of S; :: thesis: ( d _|_ & d _|_ implies d _|_ )
assume that
A1: d _|_ and
A2: d _|_ ; :: thesis: d _|_
d _|_ by A1, Th6;
then d _|_ by VECTSP_1:17;
then d _|_ by A2, Def1;
then d _|_ by RLVECT_1:def 3;
then d _|_ by RLVECT_1:def 3;
then d _|_ by RLVECT_1:5;
hence d _|_ by RLVECT_1:4; :: thesis: verum