let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y st ERl PA = ERl PB holds
PA = PB
let PA, PB be a_partition of Y; :: thesis: ( ERl PA = ERl PB implies PA = PB )
assume A1: ERl PA = ERl PB ; :: thesis: PA = PB
A2: ( PA '<' PB & PB '<' PA ) by A1, Th24;
thus PA = PB by A2, Th5; :: thesis: verum