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
A1: v in PA and
u2 in PA and
A2: 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 ; :: thesis: verum
end;
then A3: (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 A4: u in PA ; :: thesis: ex v being set st
( v in (INTERSECTION (PA,PA)) \ & u c= v )

then A5: u <> {} by EQREL_1:def 4;
set v = u /\ u;
A6: not u /\ u in by ;
u /\ u in INTERSECTION (PA,PA) by ;
then u /\ u in (INTERSECTION (PA,PA)) \ by ;
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 ; :: thesis: verum