defpred S1[ object , object ] means ex x9, y9 being bag of n st
( x9 = $1 & y9 = $2 & x9 divides y9 );
consider IR being Relation of (Bags n),(Bags n) such that
A1:
for x, y being object holds
( [x,y] in IR iff ( x in Bags n & y in Bags n & S1[x,y] ) )
from RELSET_1:sch 1();
set IT = RelStr(# (Bags n),IR #);
reconsider IT = RelStr(# (Bags n),IR #) as strict RelStr ;
take
IT
; ( the carrier of IT = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of IT iff x divides y ) ) )
thus
the carrier of IT = Bags n
; for x, y being bag of n holds
( [x,y] in the InternalRel of IT iff x divides y )
let x, y be bag of n; ( [x,y] in the InternalRel of IT iff x divides y )
assume A2:
x divides y
; [x,y] in the InternalRel of IT
A3:
x in Bags n
by PRE_POLY:def 12;
y in Bags n
by PRE_POLY:def 12;
hence
[x,y] in the InternalRel of IT
by A1, A2, A3; verum