let p, q, r, s be non zero Point of (TOP-REAL 3); :: thesis: ( 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 )
assume (p <X> q) <X> (r <X> s) is zero ; :: thesis: ( are_Prop p,q or are_Prop r,s or are_Prop p <X> q,r <X> s )
then ( p <X> q is zero or r <X> s is zero or are_Prop p <X> q,r <X> s ) by Th43;
hence ( are_Prop p,q or are_Prop r,s or are_Prop p <X> q,r <X> s ) by Th43; :: thesis: verum