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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in PB or x in PA )
reconsider xx = x as set by TARSKI:1;
assume A3: x in PB ; :: thesis: x in PA
then consider V being set such that
A4: V in PA and
A5: xx c= V by A1, 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;
x = W by A3, A5, A6, A7, Th1, XBOOLE_1:1;
hence x in PA by A4, A5, A7, XBOOLE_0:def 10; :: thesis: verum