let A be set ; :: thesis: for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
D ^ B c= D ^ C
let B, C, D be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( B c= C implies D ^ B c= D ^ C )
( D ^ C = C ^ D & D ^ B = B ^ D ) by Th48;
hence ( B c= C implies D ^ B c= D ^ C ) by Th46; :: thesis: verum