defpred S₁[ object ] 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 object 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 ) ) ) by A1, PARTFUN1:45;
defpred S₂[ object , object ] 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
A3: for c, d being object holds
( [c,d] in R iff ( c in S & d in S & S₂[c,d] ) ) from RELSET_1:sch 1();
A4: for c, d being object 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 object ; :: 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 A5: [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 A6: c in S by A3;
A7: d in S by A3, A5;
ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & f <= g ) by A3, A5;
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 A6, A7; :: thesis: verum

end;

given f, g being Function of L,(InclPoset (Ids L)) such that A8: c = f and
A9: d = g and
A10: c in S and
A11: d in S and
A12: f <= g ; :: thesis: [c,d] in R
thus [c,d] in R by A3, A8, A9, A10, A11, A12; :: 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 object 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 object 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, A4; :: thesis: verum