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 #); ( 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()
; 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; 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; ( x ==> p iff P1[x,p] )
hereby ( P1[x,p] implies x ==> p )
end;
assume A2:
P1[x,p]
; 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; verum