defpred S1[ 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))) & S1[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 S2[ 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 & S2[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 ;
( [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 ( 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
;
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;
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
;
[c,d] in R
thus
[c,d] in R
by A3, A8, A9, A10, A11, A12;
verum
end;
take
RelStr(# S,R #)
; 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; verum