let i1, i2 be Element of I; :: thesis: ( not B . i1 is trivial & not B . i2 is trivial implies i1 = i2 )
assume that
A5: not B . i1 is trivial and
A6: not B . i2 is trivial ; :: thesis: i1 = i2
consider i being Element of I such that
A7: 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 A5, A7
.= i2 by A6, A7 ; :: thesis: verum