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

union IT is Subset of R ;

hence ex b_{1} being Subset of R st b_{1} = union { S where S is Subset of R : ( S is well_founded & S is lower ) }
; :: thesis: verum

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

proof

then reconsider IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } as Subset-Family of R ;
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;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

union IT is Subset of R ;

hence ex b