thus R \/ S c= [:(R1 \/ S1),(R2 \/ S2):] by ZFMISC_1:143; :: according to RELSET_1:def 1 :: thesis: verum