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

B: now

assume S1: 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 set st x in X holds
x in the carrier of R by A;
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 A;
hence ( x in X iff x is_maximal_in the carrier of R ) by A, S1; :: thesis: verum

end;

now

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 B; :: thesis: verum