let F be Field; 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; 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; ( 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 _|_
; ( not a _|_ & not b _|_ )
assume
( a _|_ or b _|_ )
; 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; verum