theorem Th8: :: ANPROJ11:8

for a, u, v being non zero Element of (TOP-REAL 3) st not are_Prop u,v & |(a,u)| = 0 & |(a,v)| = 0 holds
are_Prop a,u <X> v