defpred S_{1}[ object ] means ( P_{1}[$1] & $1 is Element of F_{1}() );

_{2}(), the InternalRel of F_{2}() #) = RelStr(# the carrier of F_{3}(), the InternalRel of F_{3}() #)
from WAYBEL10:sch 3(A4, A3); :: thesis: verum

A3: now :: thesis: for x being object holds

( x is Element of F_{3}() iff S_{1}[x] )

( x is Element of F

let x be object ; :: thesis: ( x is Element of F_{3}() iff S_{1}[x] )

( x is Element of F_{3}() implies x is Element of F_{1}() )
by YELLOW_0:58;

hence ( x is Element of F_{3}() iff S_{1}[x] )
by A2; :: thesis: verum

end;( x is Element of F

hence ( x is Element of F

A4: now :: thesis: for x being object holds

( x is Element of F_{2}() iff S_{1}[x] )

thus
RelStr(# the carrier of F( x is Element of F

let x be object ; :: thesis: ( x is Element of F_{2}() iff S_{1}[x] )

( x is Element of F_{2}() implies x is Element of F_{1}() )
by YELLOW_0:58;

hence ( x is Element of F_{2}() iff S_{1}[x] )
by A1; :: thesis: verum

end;( x is Element of F

hence ( x is Element of F