defpred S₁[ set ] means ex a, b being Element of E ^omega st
( a in A & b in B & $1 = a ^ b );
consider C being Subset of (E ^omega) such that
A1: for x being set holds
( x in C iff ( x in E ^omega & S₁[x] ) ) from SUBSET_1:sch 1();
take C ; :: thesis: for x being set holds
( x in C iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) )
thus for x being set holds
( x in C iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) by A1; :: thesis: verum