let X be non empty set ; :: thesis: for C, x being set st C is Classification of X & x in union C holds
x c= X
let C, x be set ; :: thesis: ( C is Classification of X & x in union C implies x c= X )
assume that
A1: C is Classification of X and
A2: x in union C ; :: thesis: x c= X
consider Y being set such that
A3: x in Y and
A4: Y in C by A2, TARSKI:def 4;
reconsider Y9 = Y as a_partition of X by A1, A4, PARTIT1:def 3;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in X )
assume a in x ; :: thesis: a in X
then a in union Y9 by A3, TARSKI:def 4;
hence a in X ; :: thesis: verum