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

proof

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