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

A7: 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_maximal_in the carrier of R ) )

assume A8: 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_maximal_in the carrier of R )
for x being object st x in X holds
x in the carrier of R by A6;
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_maximal_in the carrier of R )
let x be Element of R; :: thesis: ( x in X iff x is_maximal_in the carrier of R )
( x in X implies S₁[x] ) by A6;
hence ( x in X iff x is_maximal_in the carrier of R ) by A6, A8; :: 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_maximal_in [#] R ) ) & ( R is empty implies ex b₁ being Subset of R st b₁ = {} ) ) by A7; :: thesis: verum