thus ( X c= Y implies for n being natural number st n in X holds
n in Y ) ; :: thesis: ( ( for n being natural number st n in X holds
n in Y ) implies X c= Y )
assume A1: for n being natural number st n in X holds
n in Y ; :: thesis: X c= Y
let i be integer number ; :: according to MEMBERED:def 11 :: thesis: ( i in X implies i in Y )
assume i in X ; :: thesis: i in Y
hence i in Y by A1; :: thesis: verum