let IT1, IT2 be Element of F; :: thesis: ( ( ex p being Element of S st

( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies IT1 = IT2 ) & ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) )

thus ( ex p being Element of S st

( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies IT1 = IT2 ) :: thesis: ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 )

( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) ; :: thesis: verum

( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies IT1 = IT2 ) & ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) )

thus ( ex p being Element of S st

( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds

IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies IT1 = IT2 ) :: thesis: ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 )

proof

thus
( ( for p being Element of S holds
given p being Element of S such that A3:
( not a _|_ & not x _|_ )
; :: thesis: ( ex q being Element of S st

( not a _|_ & not x _|_ & not IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) or ex q being Element of S st

( not a _|_ & not x _|_ & not IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) or IT1 = IT2 )

consider r being Element of S such that

A4: ( not a _|_ & not x _|_ ) by A3;

assume that

A5: for q being Element of S st not a _|_ & not x _|_ holds

IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) and

A6: for q being Element of S st not a _|_ & not x _|_ holds

IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ; :: thesis: IT1 = IT2

IT1 = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)) by A5, A4;

hence IT1 = IT2 by A6, A4; :: thesis: verum

end;( not a _|_ & not x _|_ & not IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) or ex q being Element of S st

( not a _|_ & not x _|_ & not IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) or IT1 = IT2 )

consider r being Element of S such that

A4: ( not a _|_ & not x _|_ ) by A3;

assume that

A5: for q being Element of S st not a _|_ & not x _|_ holds

IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) and

A6: for q being Element of S st not a _|_ & not x _|_ holds

IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ; :: thesis: IT1 = IT2

IT1 = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)) by A5, A4;

hence IT1 = IT2 by A6, A4; :: thesis: verum

( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) ; :: thesis: verum