let F be Field; :: thesis: for S being SymSp of F
for a', a, b, b' 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', a, b, b' being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
let a', a, b, b' be Element of S; :: thesis: ( not a _|_ & b _|_ & not b _|_ & a _|_ implies ( not a _|_ & not b _|_ ) )
set 0V = 0. S;
assume A1: ( not a _|_ & b _|_ & not b _|_ & a _|_ ) ; :: thesis: ( not a _|_ & not b _|_ )
assume ( a _|_ or b _|_ ) ; :: thesis: contradiction
then ( ( a _|_ & a _|_ ) or ( b _|_ & b _|_ ) ) by A1, Def1;
then ( ( a _|_ & a _|_ ) or ( b _|_ & b _|_ ) ) by VECTSP_1:59;
then ( a _|_ or b _|_ ) by Def1;
then ( a _|_ or b _|_ ) by RLVECT_1:def 6;
then ( a _|_ or b _|_ ) by RLVECT_1:16;
hence contradiction by A1, RLVECT_1:10; :: thesis: verum