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
A1: 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 A2: u in (INTERSECTION PA,PA) \ {{} } ; :: thesis: ex v being set st
( v in PA & u c= v )
consider v, u2 being set such that
A3: v in PA and
u2 in PA and
A4: u = v /\ u2 by A2, 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;

A5: (INTERSECTION PA,PA) \ {{} } '<' PA by A1, SETFAM_1:def 2;
A6: 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 )
A8: u <> {} by A7, EQREL_1:def 6;
set v = u /\ u;
A9: not u /\ u in {{} } by A8, TARSKI:def 1;
A10: u /\ u in INTERSECTION PA,PA by A7, SETFAM_1:def 5;
A11: u /\ u in (INTERSECTION PA,PA) \ {{} } by A9, A10, XBOOLE_0:def 5;
thus ex v being set st
( v in (INTERSECTION PA,PA) \ {{} } & u c= v ) by A11; :: thesis: verum

end;

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