let F be Field; :: thesis: for S being SymSp of F
for a, b, a9, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
let S be SymSp of F; :: thesis: for a, b, a9, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
let a, b, a9, b9 be Element of S; :: thesis: ( not a _|_ & b _|_ & not b _|_ & a _|_ implies ( not a _|_ & not b _|_ ) )
set 0V = 0. S;
assume that
A1: not a _|_ and
A2: b _|_ and
A3: not b _|_ and
A4: a _|_ ; :: thesis: ( not a _|_ & not b _|_ )
assume ( a _|_ or b _|_ ) ; :: thesis: contradiction
then ( ( a _|_ & a _|_ ) or ( b _|_ & b _|_ ) ) by A2, A4, Def1;
then ( ( a _|_ & a _|_ ) or ( b _|_ & b _|_ ) ) by VECTSP_1:14;
then ( a _|_ or b _|_ ) by Def1;
then ( a _|_ or b _|_ ) by RLVECT_1:def 3;
then ( a _|_ or b _|_ ) by RLVECT_1:5;
hence contradiction by A1, A3, RLVECT_1:4; :: thesis: verum