defpred S₁[ set ] means $1 is_maximal_wrt X,R;
consider I being set such that
A1: for x being set holds
( x in I iff ( x in X & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being set 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 set holds
( x in I iff x is_maximal_wrt X,R )
let x be set ; :: 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
then x in X by WAYBEL_4:def 23;
hence x in I by A1, A2; :: thesis: verum