let A be set ; :: thesis: for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
B ^ D c= C ^ D
let B, C, D be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( B c= C implies B ^ D c= C ^ D )
deffunc H₁( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
defpred S₁[ set , set ] means ( $1 in B & $2 in D );
defpred S₂[ set , set ] means ( $1 in C & $2 in D );
set X1 = { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : S₁[s,t] } ;
set X2 = { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } ;
assume B c= C ; :: thesis: B ^ D c= C ^ D
then A1: for s, t being Element of DISJOINT_PAIRS A st S₁[s,t] holds
S₂[s,t] ;
{ H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : S₁[s,t] } c= { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } from FRAENKEL:sch 2(A1);
hence B ^ D c= C ^ D by XBOOLE_1:26; :: thesis: verum