let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q & ( p `1 = q `1 or p `2 = q `2 ) implies <*p,q*> is being_S-Seq )
assume that
A1: p <> q and
A2: ( p `1 = q `1 or p `2 = q `2 ) ; :: thesis: <*p,q*> is being_S-Seq
set f = <*p,q*>;
thus <*p,q*> is one-to-one by A1, FINSEQ_3:103; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len <*p,q*> & <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special )
thus len <*p,q*> >= 2 by FINSEQ_1:61; :: thesis: ( <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special )
thus ( <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special ) by A2, Lm2, Lm6, Th40; :: thesis: verum