defpred S₁[ 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 & S₁[x,y] ) ) from RELSET_1:sch 1();
set IT = RelStr(# (Bags n),IR #);
reconsider IT = RelStr(# (Bags n),IR #) as strict RelStr ;
take IT ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( [x,y] in the InternalRel of IT iff x divides y )

hereby :: thesis: ( x divides y implies [x,y] in the InternalRel of IT )

assume [x,y] in the InternalRel of IT ; :: thesis: x divides y
then ex x9, y9 being bag of n st
( x9 = x & y9 = y & x9 divides y9 ) by A1;
hence x divides y ; :: thesis: verum

end;

assume A2: x divides y ; :: thesis: [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; :: thesis: verum