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

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