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 b1 being Subset of R st
for b being Element of R holds
( b in b1 iff b is_associated_to a ) by A1; :: thesis: verum