let F be Field; :: thesis: for S being SymSp of F
for a, b, c being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
let S be SymSp of F; :: thesis: for a, b, c being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
let a, b, c be Element of S; :: thesis: ( c _|_ or not c _|_ or not c _|_ )
set 1F = 1_ F;
assume A1: not c _|_ ; :: thesis: ( not c _|_ or not c _|_ )
assume A2: ( c _|_ & c _|_ ) ; :: thesis: contradiction
then c _|_ by VECTSP_1:def 15;
then c _|_ ;
then c _|_ ;
then c _|_ by RLVECT_1:def 3;
hence contradiction by A1, A2, Th4; :: thesis: verum