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
B . j is 1 -element by Def20;
A8: not B . i2 is 1 -element by A6;
not B . i1 is 1 -element by A5;
hence i1 = i by A7
.= i2 by A7, A8 ;
:: thesis: verum