defpred S_{1}[ 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_{1}[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 )

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

( 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

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 A2:
x divides y
; :: thesis: [x,y] in the InternalRel of ITassume
[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;then ex x9, y9 being bag of n st

( x9 = x & y9 = y & x9 divides y9 ) by A1;

hence x divides y ; :: thesis: verum

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