let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds

a in C ) holds

B c= C

let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( ( for a being Element of DISJOINT_PAIRS A st a in B holds

a in C ) implies B c= C )

assume A1: for a being Element of DISJOINT_PAIRS A st a in B holds

a in C ; :: thesis: B c= C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )

assume A2: x in B ; :: thesis: x in C

then x is Element of DISJOINT_PAIRS A by SETWISEO:9;

hence x in C by A1, A2; :: thesis: verum

a in C ) holds

B c= C

let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( ( for a being Element of DISJOINT_PAIRS A st a in B holds

a in C ) implies B c= C )

assume A1: for a being Element of DISJOINT_PAIRS A st a in B holds

a in C ; :: thesis: B c= C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )

assume A2: x in B ; :: thesis: x in C

then x is Element of DISJOINT_PAIRS A by SETWISEO:9;

hence x in C by A1, A2; :: thesis: verum