consider PR being Relation of F₁(),(F₁() *) such that
A1: for x, y being object holds
( [x,y] in PR iff ( x in F₁() & y in F₁() * & P₁[x,y] ) ) from RELSET_1:sch 1();
take DT = DTConstrStr(# F₁(),PR #); :: thesis: ( the carrier of DT = F₁() & ( for x being Symbol of DT
for p being FinSequence of the carrier of DT holds
( x ==> p iff P₁[x,p] ) ) )
thus the carrier of DT = F₁() ; :: thesis: for x being Symbol of DT
for p being FinSequence of the carrier of DT holds
( x ==> p iff P₁[x,p] )
let x be Symbol of DT; :: thesis: for p being FinSequence of the carrier of DT holds
( x ==> p iff P₁[x,p] )
let p be FinSequence of the carrier of DT; :: thesis: ( x ==> p iff P₁[x,p] )

hereby :: thesis: ( P₁[x,p] implies x ==> p )

assume x ==> p ; :: thesis: P₁[x,p]
then [x,p] in the Rules of DT by LANG1:def 1;
hence P₁[x,p] by A1; :: thesis: verum

end;

assume A2: P₁[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