defpred S₁[ object ] means ex a being Element of R st
( a = $1 & a is_minimal_in the carrier of R );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in the carrier of R & S₁[x] ) ) from XBOOLE_0:sch 1();

A2: now :: thesis: ( not the carrier of R is empty implies ex X being Subset of R st
for x being Element of R holds
( x in X iff x is_minimal_in the carrier of R ) )

assume A3: not the carrier of R is empty ; :: thesis: ex X being Subset of R st
for x being Element of R holds
( x in X iff x is_minimal_in the carrier of R )
for x being object st x in X holds
x in the carrier of R by A1;
then reconsider X = X as Subset of R by TARSKI:def 3;
take X = X; :: thesis: for x being Element of R holds
( x in X iff x is_minimal_in the carrier of R )
let x be Element of R; :: thesis: ( x in X iff x is_minimal_in the carrier of R )
( x in X implies S₁[x] ) by A1;
hence ( x in X iff x is_minimal_in the carrier of R ) by A1, A3; :: thesis: verum

end;

now :: thesis: ex X being Subset of R st X = {}

reconsider X = {} as Subset of R by XBOOLE_1:2;
take X = X; :: thesis: X = {}
thus X = {} ; :: thesis: verum

end;

hence ( ( not R is empty implies ex b₁ being Subset of R st
for x being Element of R holds
( x in b₁ iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b₁ being Subset of R st b₁ = {} ) ) by A2; :: thesis: verum