defpred S₁[ object ] means $1 is dyadic-like Rational;
consider X being set such that
A1: for o being object holds
( o in X iff ( o in RAT & S₁[o] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for o being object holds
( o in X iff o is dyadic-like Rational )
let o be object ; :: thesis: ( o in X iff o is dyadic-like Rational )
thus ( o in X iff o is dyadic-like Rational ) by A1, RAT_1:def 2; :: thesis: verum