consider I being set such that
A1: for x being object holds
( x in I iff ( x in X & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object st x in I holds
x in X by A1;
then reconsider I = I as Subset of X by TARSKI:def 3;
take I ; :: thesis: for x being object holds
( x in I iff x is_maximal_wrt X,R )
let x be object ; :: thesis: ( x in I iff x is_maximal_wrt X,R )
thus ( x in I implies x is_maximal_wrt X,R ) by A1; :: thesis: ( x is_maximal_wrt X,R implies x in I )
assume A2: x is_maximal_wrt X,R ; :: thesis: x in I
thus x in I by A1, A2; :: thesis: verum