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

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

hence
B c= B ^ B
by Lm5; :: thesis: veruma 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;a = a \/ a ;

hence ( a in B implies a in B ^ B ) by Th35; :: thesis: verum