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 )
proof
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;
hence PA '>' PA '/\' PB by SETFAM_1:def 2; :: thesis: verum