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
A1: for u being set st u in PA '/\' PB holds
ex v being set st
( v in PA & u c= v )

proof

let u be set ; :: thesis: ( u in PA '/\' PB implies ex v being set st
( v in PA & u c= v ) )
assume A2: u in PA '/\' PB ; :: thesis: ex v being set st
( v in PA & u c= v )
consider u1, u2 being set such that
A3: u1 in PA and
u2 in PB and
A4: u = u1 /\ u2 by A2, SETFAM_1:def 5;
take u1 ; :: thesis: ( u1 in PA & u c= u1 )
thus ( u1 in PA & u c= u1 ) by A3, A4, XBOOLE_1:17; :: thesis: verum

end;

thus PA '>' PA '/\' PB by A1, SETFAM_1:def 2; :: thesis: verum