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 )

for u being set st u in PA holds

ex v being set st

( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v )

hence PA '/\' PA = PA by A3, Th4; :: thesis: verum

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

then A3:
(INTERSECTION (PA,PA)) \ {{}} '<' PA
by SETFAM_1:def 2;
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 A1, A2, XBOOLE_1:17; :: thesis: verum

end;( 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 A1, A2, XBOOLE_1:17; :: thesis: verum

for u being set st u in PA holds

ex v being set st

( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v )

proof

then
PA '<' (INTERSECTION (PA,PA)) \ {{}}
by SETFAM_1:def 2;
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 A5, TARSKI:def 1;

u /\ u in INTERSECTION (PA,PA) by A4, SETFAM_1:def 5;

then u /\ u in (INTERSECTION (PA,PA)) \ {{}} by A6, XBOOLE_0:def 5;

hence ex v being set st

( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v ) ; :: thesis: verum

end;( 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 A5, TARSKI:def 1;

u /\ u in INTERSECTION (PA,PA) by A4, SETFAM_1:def 5;

then u /\ u in (INTERSECTION (PA,PA)) \ {{}} by A6, XBOOLE_0:def 5;

hence ex v being set st

( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v ) ; :: thesis: verum

hence PA '/\' PA = PA by A3, Th4; :: thesis: verum