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_{1} being Element of F st b_{1} = 0. F )

( a _|_ or x _|_ ) ) implies ex b_{1} being Element of F st b_{1} = 0. F )
; :: thesis: verum

( 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

proof

thus
( ( for p being Element of S holds
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;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

( a _|_ or x _|_ ) ) implies ex b