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 A1: ( C is Classification of X & x in union C ) ; :: thesis: x c= X
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in X )
assume A2: a in x ; :: thesis: a in X
consider Y being set such that
A3: ( x in Y & Y in C ) by A1, TARSKI:def 4;
reconsider Y' = Y as a_partition of X by A1, A3, PARTIT1:def 3;
a in union Y' by A2, A3, TARSKI:def 4;
hence a in X ; :: thesis: verum