[(In (r,RAT)),(In (s,RAT))] in [:RAT,RAT:] by ZFMISC_1:87;
hence In ([r,s],[:RAT,RAT:]) = [r,s] by SUBSET_1:def 8; :: thesis: verum