theorem Th57: :: BKMODEL1:68

for u, v being non zero Element of (TOP-REAL 3)
for a, b being Real st ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. (TOP-REAL 3) holds
are_Prop u,v