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

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