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

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

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 (proj D) " {p} or e in p )
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;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

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