let F be Field; :: thesis: for S being SymSp of F
for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )
let S be SymSp of F; :: thesis: for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )
let a, b be Element of S; :: thesis: ( a <> 0. S & b <> 0. S implies ex p being Element of S st
( not a _|_ & not b _|_ ) )
assume that
A1: a <> 0. S and
A2: b <> 0. S ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ )
consider a9 being Element of S such that
A3: not a _|_ by A1, Def1;

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

consider b9 being Element of S such that
A4: not b _|_ by A2, Def1;
assume A5: b _|_ ; :: thesis: ex p being Element of S st
( not a _|_ & not b _|_ )

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

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

end;

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

end;

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