set M = { b where b is Element of R : b is_associated_to a } ;

now :: thesis: for B being object st B in { b where b is Element of R : b is_associated_to a } holds
B in the carrier of R

let B be object ; :: thesis: ( B in { b where b is Element of R : b is_associated_to a } implies B in the carrier of R )

now :: thesis: ( B in { b where b is Element of R : b is_associated_to a } & B in { b where b is Element of R : b is_associated_to a } implies B in the carrier of R )

assume B in { b where b is Element of R : b is_associated_to a } ; :: thesis: ( B in { b where b is Element of R : b is_associated_to a } implies B in the carrier of R )
then ex B9 being Element of R st
( B = B9 & B9 is_associated_to a ) ;
hence ( B in { b where b is Element of R : b is_associated_to a } implies B in the carrier of R ) ; :: thesis: verum

end;

hence ( B in { b where b is Element of R : b is_associated_to a } implies B in the carrier of R ) ; :: thesis: verum

end;

then A1: { b where b is Element of R : b is_associated_to a } c= the carrier of R by TARSKI:def 3;

now :: thesis: for A being Element of R holds
( A in { b where b is Element of R : b is_associated_to a } iff A is_associated_to a )

let A be Element of R; :: thesis: ( A in { b where b is Element of R : b is_associated_to a } iff A is_associated_to a )
( A in { b where b is Element of R : b is_associated_to a } implies A is_associated_to a )

proof

assume A in { b where b is Element of R : b is_associated_to a } ; :: thesis: A is_associated_to a
then ex A9 being Element of R st
( A = A9 & A9 is_associated_to a ) ;
hence A is_associated_to a ; :: thesis: verum

end;

hence ( A in { b where b is Element of R : b is_associated_to a } iff A is_associated_to a ) ; :: thesis: verum

end;

hence ex b₁ being Subset of R st
for b being Element of R holds
( b in b₁ iff b is_associated_to a ) by A1; :: thesis: verum