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