defpred S₁[ set ] means ex s being Function of L,(InclPoset (Ids L)) st
( $1 = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) );
consider S being set such that
A1: for a being set holds
( a in S iff ( a in PFuncs the carrier of L,the carrier of (InclPoset (Ids L)) & S₁[a] ) ) from XBOOLE_0:sch 1();
A2: for a being set holds
( a in S iff ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) )

proof

let a be set ; :: thesis: ( a in S iff ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) )
thus ( a in S implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) by A1; :: thesis: ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in S )
given s being Function of L,(InclPoset (Ids L)) such that A3: ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ; :: thesis: a in S
s in PFuncs the carrier of L,the carrier of (InclPoset (Ids L)) by PARTFUN1:119;
hence a in S by A1, A3; :: thesis: verum

end;

defpred S₂[ set , set ] means ex f, g being Function of L,(InclPoset (Ids L)) st
( $1 = f & $2 = g & f <= g );
consider R being Relation of S,S such that
A4: for c, d being set holds
( [c,d] in R iff ( c in S & d in S & S₂[c,d] ) ) from RELSET_1:sch 1();
A5: for c, d being set holds
( [c,d] in R iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) )

proof

let c, d be set ; :: thesis: ( [c,d] in R iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) )

hereby :: thesis: ( ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) implies [c,d] in R )

assume A6: [c,d] in R ; :: thesis: ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g )
then A7: ( c in S & d in S ) by A4;
consider f, g being Function of L,(InclPoset (Ids L)) such that
A8: ( c = f & d = g & f <= g ) by A4, A6;
thus ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) by A7, A8; :: thesis: verum

end;

given f, g being Function of L,(InclPoset (Ids L)) such that A9: ( c = f & d = g & c in S & d in S & f <= g ) ; :: thesis: [c,d] in R
thus [c,d] in R by A4, A9; :: thesis: verum

end;

take RelStr(# S,R #) ; :: thesis: for a being set holds
( ( a in the carrier of RelStr(# S,R #) implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of RelStr(# S,R #) ) & ( for c, d being set holds
( [c,d] in the InternalRel of RelStr(# S,R #) iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of RelStr(# S,R #) & d in the carrier of RelStr(# S,R #) & f <= g ) ) ) )
thus for a being set holds
( ( a in the carrier of RelStr(# S,R #) implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of RelStr(# S,R #) ) & ( for c, d being set holds
( [c,d] in the InternalRel of RelStr(# S,R #) iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of RelStr(# S,R #) & d in the carrier of RelStr(# S,R #) & f <= g ) ) ) ) by A2, A5; :: thesis: verum