let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds PA '>' PA '/\' PB

let PA, PB be a_partition of Y; :: thesis: PA '>' PA '/\' PB

for u being set st u in PA '/\' PB holds

ex v being set st

( v in PA & u c= v )

let PA, PB be a_partition of Y; :: thesis: PA '>' PA '/\' PB

for u being set st u in PA '/\' PB holds

ex v being set st

( v in PA & u c= v )

proof

hence
PA '>' PA '/\' PB
by SETFAM_1:def 2; :: thesis: verum
let u be set ; :: thesis: ( u in PA '/\' PB implies ex v being set st

( v in PA & u c= v ) )

assume u in PA '/\' PB ; :: thesis: ex v being set st

( v in PA & u c= v )

then consider u1, u2 being set such that

A1: u1 in PA and

u2 in PB and

A2: u = u1 /\ u2 by SETFAM_1:def 5;

take u1 ; :: thesis: ( u1 in PA & u c= u1 )

thus ( u1 in PA & u c= u1 ) by A1, A2, XBOOLE_1:17; :: thesis: verum

end;( v in PA & u c= v ) )

assume u in PA '/\' PB ; :: thesis: ex v being set st

( v in PA & u c= v )

then consider u1, u2 being set such that

A1: u1 in PA and

u2 in PB and

A2: u = u1 /\ u2 by SETFAM_1:def 5;

take u1 ; :: thesis: ( u1 in PA & u c= u1 )

thus ( u1 in PA & u c= u1 ) by A1, A2, XBOOLE_1:17; :: thesis: verum