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 that
A1: (1_ F) + (1_ F) <> 0. F and
A2: a <> 0. S and
A3: b <> 0. S and
A4: c <> 0. S ; :: thesis: 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;

now :: thesis: ( c _|_ & b _|_ implies ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) )

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

A11: now :: thesis: ( not a _|_ implies ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) )

c _|_ by A9, Def1;
then A12: not c _|_ by A8, Th4;
not b _|_ by A1, A6, Th5;
then A13: not b _|_ by A10, Th4;
assume not a _|_ ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A13, A12; :: thesis: verum

end;

now :: thesis: ( not a _|_ implies ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) )

assume A14: not a _|_ ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
( not b _|_ & not c _|_ ) by A6, A8, A9, A10, Th4;
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A14; :: thesis: verum

end;

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

end;

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