set M = { [a,b] where a, b is Element of I : b <> 0. I } ;
for u being object st u in { [a,b] where a, b is Element of I : b <> 0. I } holds
u in [: the carrier of I, the carrier of I:]

proof

let u be object ; :: thesis: ( u in { [a,b] where a, b is Element of I : b <> 0. I } implies u in [: the carrier of I, the carrier of I:] )
assume u in { [a,b] where a, b is Element of I : b <> 0. I } ; :: thesis: u in [: the carrier of I, the carrier of I:]
then ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ;
hence u in [: the carrier of I, the carrier of I:] ; :: thesis: verum

end;

then A1: { [a,b] where a, b is Element of I : b <> 0. I } is Subset of [: the carrier of I, the carrier of I:] by TARSKI:def 3;
for u being set holds
( u in { [a,b] where a, b is Element of I : b <> 0. I } iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ;
hence ex b₁ being Subset of [: the carrier of I, the carrier of I:] st
for u being set holds
( u in b₁ iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) by A1; :: thesis: verum