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, Th26; :: 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