take TOP-REAL 1 ; :: thesis: ( TOP-REAL 1 is constituted-FinSeqs & not TOP-REAL 1 is empty & TOP-REAL 1 is strict )
thus ( TOP-REAL 1 is constituted-FinSeqs & not TOP-REAL 1 is empty & TOP-REAL 1 is strict ) ; :: thesis: verum