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