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 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