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 set ; :: according to TARSKI:def 3 :: thesis: ( not e in (proj D) " A or e in union A )
assume A1: e in (proj D) " A ; :: thesis: e in union A
then A2: (proj D) . e in A by FUNCT_2:46;
e in (proj D) . e by A1, Def1;
hence e in union A by A2, TARSKI:def 4; :: thesis: verum

end;

let e be set ; :: 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
A3: ( e in u & u in A ) by TARSKI:def 4;
A4: u in D by A3;
then (proj D) . e = u by A3, Th29;
hence e in (proj D) " A by A3, A4, FUNCT_2:46; :: thesis: verum