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();
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 C holds
ex p, r being set st o = [p,r] by A1;
then reconsider C' = C as Relation by RELAT_1:def 1;
for o being set st o in D holds
ex p, r being set st o = [p,r] by A2;
then reconsider D' = D as Relation by RELAT_1:def 1;
reconsider F = C' * D' as set ;
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 ) )

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;
consider r being set such that
A6: ( [q,r] in C' & [r,s] in D' ) by A4, A5, RELAT_1:def 8;
take q = q; :: thesis: ex r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B )
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, A6; :: thesis: verum

end;

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 A7: ( p = [q,s] & [q,r] in A & [r,s] in B ) ; :: thesis: p in F
A8: [q,r] in C' by A1, A7;
[r,s] in D' by A2, A7;
hence p in F by A7, 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