theorem Th4: :: MENELAUS:4

for A, B being Point of (TOP-REAL 2)
for lambda, mu being Real holds
( ((lambda * A) + (mu * B)) `1 = (lambda * (A `1)) + (mu * (B `1)) & ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2)) )