let Y be non empty set ; 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; ( PA '>' PB & PB '>' PA implies PB c= PA )
assume that
A1:
PA '>' PB
and
A2:
PB '>' PA
; PB c= PA
let x be object ; TARSKI:def 3 ( not x in PB or x in PA )
reconsider xx = x as set by TARSKI:1;
assume A3:
x in PB
; 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; verum