let A be set ; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A) holds B c= B ^ B
let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: B c= B ^ B

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in B holds
a in B ^ B

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in B implies a in B ^ B )
a = a \/ a ;
hence ( a in B implies a in B ^ B ) by Th35; :: thesis: verum

end;

hence B c= B ^ B by Lm5; :: thesis: verum