let F be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 A1: ( (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S ) ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
then consider r being Element of S such that
A2: ( not a _|_ & not b _|_ ) by Th21;
consider s being Element of S such that
A3: ( not a _|_ & not c _|_ ) by A1, Th21;

now

assume that
A4: c _|_ and
A5: b _|_ ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )

A6: now

assume A7: not a _|_ ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
( not b _|_ & not c _|_ ) by A2, A3, A4, A5, Th14;
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A7; :: thesis: verum

end;

now

assume A8: not a _|_ ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
( not b _|_ & not c _|_ )

proof

( not b _|_ & c _|_ ) by A1, A2, A4, Def1, Th15;
hence ( not b _|_ & not c _|_ ) by A3, A5, Th14; :: thesis: verum

end;

hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A8; :: thesis: verum

end;

hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A2, A6, Th19; :: thesis: verum

end;

hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A2, A3; :: thesis: verum