:: deftheorem Def5 defines standard GOBOARD5:def 5 :
for IT being non empty FinSequence of (TOP-REAL 2) holds
( IT is standard iff IT is_sequence_on GoB IT );