theorem Th45: :: BKMODEL4:52

for u, v, w being Element of (TOP-REAL 2) st u in LSeg (v,w) holds
|[(u `1),(u `2),1]| in LSeg (|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]|)