let IT1, IT2 be Element of F; ( ( 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 )
( ( 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 _|_ )
;
( 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))
;
IT1 = IT2
IT1 = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y))
by A5, A4;
hence
IT1 = IT2
by A6, A4;
verum
end;
thus
( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 )
; verum