let k, n be Nat; :: thesis: ( k in GreaterOrEqualsNumbers n iff n <= k )
thus ( k in GreaterOrEqualsNumbers n implies n <= k ) :: thesis: ( n <= k implies k in GreaterOrEqualsNumbers n )

proof

assume k in GreaterOrEqualsNumbers n ; :: thesis: n <= k
then not k in Segm n by XBOOLE_0:def 5;
hence n <= k by NAT_1:44; :: thesis: verum

end;

A1: k in NAT by ORDINAL1:def 12;
assume n <= k ; :: thesis: k in GreaterOrEqualsNumbers n
then not k in Segm n by NAT_1:44;
hence k in GreaterOrEqualsNumbers n by A1, XBOOLE_0:def 5; :: thesis: verum