let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PA = PB
let PA, PB be a_partition of Y; :: thesis: ( PA '>' PB & PB '>' PA implies PA = PB )
assume A1: ( PA '>' PB & PB '>' PA ) ; :: thesis: PA = PB
then A2: PB c= PA by Th4;
PA c= PB by A1, Th4;
hence PA = PB by A2, XBOOLE_0:def 10; :: thesis: verum