let Y be non empty set ; :: thesis: for PA being a_partition of Y holds PA '/\' PA = PA
let PA be a_partition of Y; :: thesis: PA '/\' PA = PA
for u being set st u in (INTERSECTION (PA,PA)) \ {{}} holds
ex v being set st
( v in PA & u c= v )

proof

let u be set ; :: thesis: ( u in (INTERSECTION (PA,PA)) \ {{}} implies ex v being set st
( v in PA & u c= v ) )
assume u in (INTERSECTION (PA,PA)) \ {{}} ; :: thesis: ex v being set st
( v in PA & u c= v )
then consider v, u2 being set such that
A3: v in PA and
u2 in PA and
A4: u = v /\ u2 by SETFAM_1:def 5;
take v ; :: thesis: ( v in PA & u c= v )
thus ( v in PA & u c= v ) by A3, A4, XBOOLE_1:17; :: thesis: verum

end;

then A5: (INTERSECTION (PA,PA)) \ {{}} '<' PA by SETFAM_1:def 2;
for u being set st u in PA holds
ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v )

proof

let u be set ; :: thesis: ( u in PA implies ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v ) )
assume A7: u in PA ; :: thesis: ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v )
then A8: u <> {} by EQREL_1:def 6;
set v = u /\ u;
A9: not u /\ u in {{}} by A8, TARSKI:def 1;
u /\ u in INTERSECTION (PA,PA) by A7, SETFAM_1:def 5;
then u /\ u in (INTERSECTION (PA,PA)) \ {{}} by A9, XBOOLE_0:def 5;
hence ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v ) ; :: thesis: verum

end;

then PA '<' (INTERSECTION (PA,PA)) \ {{}} by SETFAM_1:def 2;
hence PA '/\' PA = PA by A5, Th5; :: thesis: verum