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 )

proof

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;

thus ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) ; :: thesis: verum