defpred S₁[ set ] means ex p, r being set st $1 = [p,r];
consider C being set such that
A1: for o being set holds
( o in C iff ( o in A & S₁[o] ) ) from XBOOLE_0:sch 1();
for o being set st o in C holds
ex p, r being set st o = [p,r] by A1;
then reconsider C9 = C as Relation by RELAT_1:def 1;
consider D being set such that
A2: for o being set holds
( o in D iff ( o in B & S₁[o] ) ) from XBOOLE_0:sch 1();
for o being set st o in D holds
ex p, r being set st o = [p,r] by A2;
then reconsider D9 = D as Relation by RELAT_1:def 1;
reconsider F = C9 * D9 as set ;

A3: now

let p be set ; :: thesis: ( p in F implies ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) )
assume A4: p in F ; :: thesis: ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B )
then consider q, s being set such that
A5: p = [q,s] by RELAT_1:def 1;
take q = q; :: thesis: ex r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B )
consider r being set such that
A6: [q,r] in C9 and
A7: [r,s] in D9 by A4, A5, RELAT_1:def 8;
take r = r; :: thesis: ex s being set st
( p = [q,s] & [q,r] in A & [r,s] in B )
take s = s; :: thesis: ( p = [q,s] & [q,r] in A & [r,s] in B )
thus p = [q,s] by A5; :: thesis: ( [q,r] in A & [r,s] in B )
thus [q,r] in A by A1, A6; :: thesis: [r,s] in B
thus [r,s] in B by A2, A7; :: thesis: verum

end;

take F ; :: thesis: for p being set holds
( p in F iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) )

now

let p be set ; :: thesis: ( ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) implies p in F )
given q, r, s being set such that A8: p = [q,s] and
A9: ( [q,r] in A & [r,s] in B ) ; :: thesis: p in F
( [q,r] in C9 & [r,s] in D9 ) by A1, A2, A9;
hence p in F by A8, RELAT_1:def 8; :: thesis: verum

end;

hence for p being set holds
( p in F iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) ) by A3; :: thesis: verum