set i = the Element of I;
take the Element of I ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st the Element of I <> j holds
( not {A} . j is empty & {A} . j is trivial )
let j be Element of I; :: thesis: ( the Element of I <> j implies ( not {A} . j is empty & {A} . j is trivial ) )
assume the Element of I <> j ; :: thesis: ( not {A} . j is empty & {A} . j is trivial )
{A} . j = {(A . j)} by PZFMISC1:def 1;
hence ( not {A} . j is empty & {A} . j is trivial ) ; :: thesis: verum