let f be FinSequence of (TOP-REAL 2); :: thesis: ( f <> {} implies Y_axis f <> {} )
assume ( f <> {} & Y_axis f = {} ) ; :: thesis: contradiction
then ( len (Y_axis f) = len f & len f <> 0 & len (Y_axis f) = 0 ) by GOBOARD1:def 4;
hence contradiction ; :: thesis: verum