let X be non empty set ; :: thesis: for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
let D be non empty a_partition of X; :: thesis: for A being Subset of D holds (proj D) " A = union A
let A be Subset of D; :: thesis: (proj D) " A = union A
thus (proj D) " A c= union A :: according to XBOOLE_0:def 10 :: thesis: union A c= (proj D) " A

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (proj D) " A or e in union A )
assume e in (proj D) " A ; :: thesis: e in union A
then ( (proj D) . e in A & e in (proj D) . e ) by Def9, FUNCT_2:38;
hence e in union A by TARSKI:def 4; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union A or e in (proj D) " A )
assume e in union A ; :: thesis: e in (proj D) " A
then consider u being set such that
A1: e in u and
A2: u in A by TARSKI:def 4;
A3: u in D by A2;
then (proj D) . e = u by A1, Th65;
hence e in (proj D) " A by A1, A2, A3, FUNCT_2:38; :: thesis: verum