let F be Field; :: thesis: for S being SymSp of F
for a, c, b being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
let S be SymSp of F; :: thesis: for a, c, b being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
let a, c, b 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 ( c _|_ & c _|_ ) ; :: thesis: contradiction
then ( c _|_ & c _|_ ) by VECTSP_1:def 26;
then ( c _|_ & c _|_ ) by VECTSP_1:def 26;
then ( c _|_ & c _|_ ) by VECTSP_1:def 26;
then ( c _|_ & c _|_ ) by RLVECT_1:def 6;
hence contradiction by A1, Th14; :: thesis: verum