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 that
A1: PA '>' PB and
A2: 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 A3: x in PB ; :: thesis: x in PA
consider V being set such that
A4: V in PA and
A5: x c= V by A1, A3, SETFAM_1:def 2;
consider W being set such that
A6: W in PB and
A7: V c= W by A2, A4, SETFAM_1:def 2;
A8: x = W by A3, A5, A6, A7, Th1, XBOOLE_1:1;
thus x in PA by A4, A5, A7, A8, XBOOLE_0:def 10; :: thesis: verum