defpred S₁[ set ] means ex t being type of T st
( $1 = t & a in adjs t );
let X1, X2 be Subset of T; :: thesis: ( ( for x being set holds
( x in X1 iff ex t being type of T st
( x = t & a in adjs t ) ) ) & ( for x being set holds
( x in X2 iff ex t being type of T st
( x = t & a in adjs t ) ) ) implies X1 = X2 )
assume that
A5: for x being set holds
( x in X1 iff S₁[x] ) and
A6: for x being set holds
( x in X2 iff S₁[x] ) ; :: thesis: X1 = X2
thus X1 = X2 from XBOOLE_0:sch 2(A5, A6); :: thesis: verum