let F be Field; for S being SymSp of F
for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
let S be SymSp of F; for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
let a, b, c be Element of S; ( (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S implies ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) )
assume that
A1:
(1_ F) + (1_ F) <> 0. F
and
A2:
a <> 0. S
and
A3:
b <> 0. S
and
A4:
c <> 0. S
; ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
consider r being Element of S such that
A5:
not a _|_
and
A6:
not b _|_
by A2, A3, Th9;
consider s being Element of S such that
A7:
not a _|_
and
A8:
not c _|_
by A2, A4, Th9;
hence
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
by A5, A6, A7, A8; verum