let b be Nat; :: thesis: ( b > 1 iff b ! > 1 )
thus ( b > 1 implies b ! > 1 ) :: thesis: ( b ! > 1 implies b > 1 )

proof

assume b > 1 ; :: thesis: b ! > 1
then b >= 1 + 1 by NAT_1:13;
hence b ! > 1 by ASYMPT_1:55; :: thesis: verum

end;

thus ( b ! > 1 implies b > 1 ) by ASYMPT_1:56, NEWTON:13; :: thesis: verum