let i1, i2 be Element of I; :: thesis: ( not B . i1 is trivial & not B . i2 is trivial implies i1 = i2 )
assume A4: ( not B . i1 is trivial & not B . i2 is trivial ) ; :: thesis: i1 = i2
consider i being Element of I such that
A5: for j being Element of I st i <> j holds
( not B . j is empty & B . j is trivial ) by Def20;
thus i1 = i by A4, A5
.= i2 by A4, A5 ; :: thesis: verum