thus ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies ex IT being Element of F st
for q being Element of S st not a _|_ & not x _|_ holds
IT = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) :: thesis: ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b₁ being Element of F st b₁ = 0. F )

proof

given p being Element of S such that A2: ( not a _|_ & not x _|_ ) ; :: thesis: ex IT being Element of F st
for q being Element of S st not a _|_ & not x _|_ holds
IT = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y)
take ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) ; :: thesis: for q being Element of S st not a _|_ & not x _|_ holds
((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y)
let q be Element of S; :: thesis: ( not a _|_ & not x _|_ implies ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) )
assume ( not a _|_ & not x _|_ ) ; :: thesis: ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y)
hence ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) by A1, A2, Th39; :: thesis: verum

end;

thus ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b₁ being Element of F st b₁ = 0. F ) ; :: thesis: verum