let f be FinSequence of (TOP-REAL 2); :: thesis: ( f <> {} implies Y_axis f <> {} )

A1: len (Y_axis f) = len f by GOBOARD1:def 2;

assume ( f <> {} & Y_axis f = {} ) ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

A1: len (Y_axis f) = len f by GOBOARD1:def 2;

assume ( f <> {} & Y_axis f = {} ) ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum