theorem Th44: :: EUCLIDLP:44

for n being Nat
for x, y0, y1 being Element of REAL n st x _|_ y0 & y0 // y1 holds
x _|_ y1