consider PR being Relation of F1(),(F1() *) such that
A1: for x, y being object holds
( [x,y] in PR iff ( x in F1() & y in F1() * & P1[x,y] ) ) from RELSET_1:sch 1();
 take DT = DTConstrStr(# F1(),PR #); :: thesis: ( the carrier of DT = F1() & ( for x being Symbol of DT
for p being FinSequence of the carrier of DT holds
( x ==> p iff P1[x,p] ) ) )
thus the carrier of DT = F1() ; :: thesis: for x being Symbol of DT
for p being FinSequence of the carrier of DT holds
( x ==> p iff P1[x,p] )
let x be Symbol of DT; :: thesis: for p being FinSequence of the carrier of DT holds
( x ==> p iff P1[x,p] )
let p be FinSequence of the carrier of DT; :: thesis: ( x ==> p iff P1[x,p] )
hereby :: thesis: ( P1[x,p] implies x ==> p )
assume x ==> p ; :: thesis: P1[x,p]
then [x,p] in the Rules of DT by LANG1:def 1;
hence P1[x,p] by A1; :: thesis: verum
end;
assume A2: P1[x,p] ; :: thesis: x ==> p
p in the carrier of DT * by FINSEQ_1:def 11;
then [x,p] in PR by A1, A2;
hence x ==> p by LANG1:def 1; :: thesis: verum