let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PB c= PA
let PA, PB be a_partition of Y; :: thesis: ( PA '>' PB & PB '>' PA implies PB c= PA )
assume A1: ( PA '>' PB & PB '>' PA ) ; :: thesis: PB c= PA
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PB or x in PA )
assume A2: x in PB ; :: thesis: x in PA
then consider V being set such that
A3: ( V in PA & x c= V ) by A1, SETFAM_1:def 2;
consider W being set such that
A4: ( W in PB & V c= W ) by A1, A3, SETFAM_1:def 2;
x = W by A2, A3, A4, Th1, XBOOLE_1:1;
hence x in PA by A3, A4, XBOOLE_0:def 10; :: thesis: verum