let X be non empty set ; :: thesis: for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
let D be non empty a_partition of X; :: thesis: for p being Element of D holds p = (proj D) " {p}
let p be Element of D; :: thesis: p = (proj D) " {p}
thus p c= (proj D) " {p} :: according to XBOOLE_0:def 10 :: thesis: (proj D) " {p} c= p
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in p or e in (proj D) " {p} )
assume A1: e in p ; :: thesis: e in (proj D) " {p}
then (proj D) . e = p by Th65;
then (proj D) . e in {p} by TARSKI:def 1;
hence e in (proj D) " {p} by A1, FUNCT_2:38; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (proj D) " {p} or e in p )
assume A2: e in (proj D) " {p} ; :: thesis: e in p
then (proj D) . e in {p} by FUNCT_1:def 7;
then (proj D) . e = p by TARSKI:def 1;
hence e in p by A2, Def9; :: thesis: verum