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