let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for x, y, s being object st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
let X be non-empty ManySortedSet of S; :: thesis: for x, y, s being object st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
set D = DTConOSA X;
set F = PTClasses X;
A1: rng (PTClasses X) c= bool [:(TS (DTConOSA X)), the carrier of S:] by RELAT_1:def 19;
let x, y, s be object ; :: thesis: ( [x,s] in (PTClasses X) . y implies ( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S ) )
assume A2: [x,s] in (PTClasses X) . y ; :: thesis: ( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
A3: y in TS (DTConOSA X)

proof

assume not y in TS (DTConOSA X) ; :: thesis: contradiction
then not y in dom (PTClasses X) ;
hence contradiction by A2, FUNCT_1:def 2; :: thesis: verum

end;

dom (PTClasses X) = TS (DTConOSA X) by FUNCT_2:def 1;
then (PTClasses X) . y in rng (PTClasses X) by A3, FUNCT_1:3;
hence ( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S ) by A2, A1, A3, ZFMISC_1:87; :: thesis: verum