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 and
A4: s is monotone and
A5: 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, A4, A5; :: 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
A6: 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();
A7: 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 A8: [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 A9: c in S by A6;
A10: d in S by A6, A8;
ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & f <= g ) by A6, A8;
hence ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) by A9, A10; :: thesis: verum

end;

given f, g being Function of L,(InclPoset (Ids L)) such that A11: c = f and
A12: d = g and
A13: c in S and
A14: d in S and
A15: f <= g ; :: thesis: [c,d] in R
thus [c,d] in R by A6, A11, A12, A13, A14, A15; :: 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, A7; :: thesis: verum