defpred S_{1}[ object ] means $1 is RoughSet of X;

consider F being set such that

A1: for x being object holds

( x in F iff ( x in [:(bool the carrier of X),(bool the carrier of X):] & S_{1}[x] ) )
from XBOOLE_0:sch 1();

take F ; :: thesis: for x being set holds

( x in F iff x is RoughSet of X )

let x be set ; :: thesis: ( x in F iff x is RoughSet of X )

thus ( x in F implies x is RoughSet of X ) by A1; :: thesis: ( x is RoughSet of X implies x in F )

assume x is RoughSet of X ; :: thesis: x in F

hence x in F by A1; :: thesis: verum

consider F being set such that

A1: for x being object holds

( x in F iff ( x in [:(bool the carrier of X),(bool the carrier of X):] & S

take F ; :: thesis: for x being set holds

( x in F iff x is RoughSet of X )

let x be set ; :: thesis: ( x in F iff x is RoughSet of X )

thus ( x in F implies x is RoughSet of X ) by A1; :: thesis: ( x is RoughSet of X implies x in F )

assume x is RoughSet of X ; :: thesis: x in F

hence x in F by A1; :: thesis: verum