for p, q, r, s being non zero Point of (TOP-REAL 3) holds
( not (p <X> q) <X> (r <X> s) is zero or are_Prop p,q or are_Prop r,s or are_Prop p <X> q,r <X> s )