set IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } ;
{ S where S is Subset of R : ( S is well_founded & S is lower ) } c= bool the carrier of R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Subset of R : ( S is well_founded & S is lower ) } or x in bool the carrier of R )
assume x in { S where S is Subset of R : ( S is well_founded & S is lower ) } ; :: thesis: x in bool the carrier of R
then ex S being Subset of R st
( x = S & S is well_founded & S is lower ) ;
hence x in bool the carrier of R ; :: thesis: verum

end;

then reconsider IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } as Subset-Family of R ;
union IT is Subset of R ;
hence ex b₁ being Subset of R st b₁ = union { S where S is Subset of R : ( S is well_founded & S is lower ) } ; :: thesis: verum