let F be Field; for S being OrtSp of F
for a, b, x, y being Element of S st not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
let S be OrtSp of F; for a, b, x, y being Element of S st not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
let a, b, x, y be Element of S; ( not a _|_ & x = 0. S implies PProJ (a,b,x,y) = 0. F )
assume that
A1:
not a _|_
and
A2:
x = 0. S
; PProJ (a,b,x,y) = 0. F
for p being Element of S holds
( a _|_ or x _|_ )
by A2, Th1, Th2;
hence
PProJ (a,b,x,y) = 0. F
by A1, Def3; verum