set f = the being_S-Seq FinSequence of (TOP-REAL 2);
( the being_S-Seq FinSequence of (TOP-REAL 2) is one-to-one & the being_S-Seq FinSequence of (TOP-REAL 2) is unfolded & the being_S-Seq FinSequence of (TOP-REAL 2) is s.n.c. & the being_S-Seq FinSequence of (TOP-REAL 2) is special & not the being_S-Seq FinSequence of (TOP-REAL 2) is trivial ) ;
hence ex b₁ being FinSequence of (TOP-REAL 2) st
( b₁ is one-to-one & b₁ is unfolded & b₁ is s.n.c. & b₁ is special & not b₁ is trivial ) ; :: thesis: verum