defpred S1[ set , set ] means ex AR being auxiliary Relation of L st
( AR = $2 & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = $1 & x' in s' . y' ) ) ) );
A1:
for a being set st a in the carrier of (MonSet L) holds
ex b being set st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
proof
let a be
set ;
:: thesis: ( a in the carrier of (MonSet L) implies ex b being set st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] ) )
assume A2:
a in the
carrier of
(MonSet L)
;
:: thesis: ex b being set st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
defpred S2[
set ,
set ]
means ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = $1 &
y' = $2 &
s' = a &
x' in s' . y' );
consider R being
Relation of the
carrier of
L,the
carrier of
L such that A3:
for
x,
y being
set holds
(
[x,y] in R iff (
x in the
carrier of
L &
y in the
carrier of
L &
S2[
x,
y] ) )
from RELSET_1:sch 1();
reconsider R =
R as
Relation of
L ;
now thus
R is
auxiliary(i)
:: thesis: ( R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) )proof
let x,
y be
Element of
L;
:: according to WAYBEL_4:def 4 :: thesis: ( [x,y] in R implies x <= y )
assume
[x,y] in R
;
:: thesis: x <= y
then consider x',
y' being
Element of
L,
s' being
Function of
L,
(InclPoset (Ids L)) such that A4:
(
x' = x &
y' = y &
s' = a &
x' in s' . y' )
by A3;
consider s being
Function of
L,
(InclPoset (Ids L)) such that A5:
(
a = s &
s is
monotone & ( for
x being
Element of
L holds
s . x c= downarrow x ) )
by A2, Def14;
s' . y c= downarrow y
by A4, A5;
hence
x <= y
by A4, WAYBEL_0:17;
:: thesis: verum
end; thus
R is
auxiliary(ii)
:: thesis: ( R is auxiliary(iii) & R is auxiliary(iv) )proof
let x,
y,
z,
u be
Element of
L;
:: according to WAYBEL_4:def 5 :: thesis: ( u <= x & [x,y] in R & y <= z implies [u,z] in R )
assume A6:
(
u <= x &
[x,y] in R &
y <= z )
;
:: thesis: [u,z] in R
then consider x',
y' being
Element of
L,
s' being
Function of
L,
(InclPoset (Ids L)) such that A7:
(
x' = x &
y' = y &
s' = a &
x' in s' . y' )
by A3;
consider s being
Function of
L,
(InclPoset (Ids L)) such that A8:
(
a = s &
s is
monotone & ( for
x being
Element of
L holds
s . x c= downarrow x ) )
by A2, Def14;
reconsider sy =
s . y,
sz =
s . z as
Element of
(InclPoset (Ids L)) ;
sy <= sz
by A6, A8, ORDERS_3:def 5;
then A9:
s . y c= s . z
by YELLOW_1:3;
s . z in the
carrier of
(InclPoset (Ids L))
;
then
s . z in Ids L
by YELLOW_1:1;
then consider sz being
Ideal of
L such that A10:
s . z = sz
;
u in sz
by A6, A7, A8, A9, A10, WAYBEL_0:def 19;
hence
[u,z] in R
by A3, A8, A10;
:: thesis: verum
end; thus
R is
auxiliary(iii)
:: thesis: R is auxiliary(iv) proof
let x,
y,
z be
Element of
L;
:: according to WAYBEL_4:def 6 :: thesis: ( [x,z] in R & [y,z] in R implies [(x "\/" y),z] in R )
assume A11:
(
[x,z] in R &
[y,z] in R )
;
:: thesis: [(x "\/" y),z] in R
then consider x1,
z1 being
Element of
L,
s1 being
Function of
L,
(InclPoset (Ids L)) such that A12:
(
x1 = x &
z1 = z &
s1 = a &
x1 in s1 . z1 )
by A3;
consider y2,
z2 being
Element of
L,
s2 being
Function of
L,
(InclPoset (Ids L)) such that A13:
(
y2 = y &
z2 = z &
s2 = a &
y2 in s2 . z2 )
by A3, A11;
s1 . z in the
carrier of
(InclPoset (Ids L))
;
then
s1 . z in Ids L
by YELLOW_1:1;
then consider sz being
Ideal of
L such that A14:
s1 . z = sz
;
consider z3 being
Element of
L such that A15:
(
z3 in sz &
x <= z3 &
y <= z3 )
by A12, A13, A14, WAYBEL_0:def 1;
ex
q being
Element of
L st
(
x <= q &
y <= q & ( for
c being
Element of
L st
x <= c &
y <= c holds
q <= c ) )
by LATTICE3:def 10;
then
x "\/" y <= z3
by A15, LATTICE3:def 13;
then
x "\/" y in sz
by A15, WAYBEL_0:def 19;
hence
[(x "\/" y),z] in R
by A3, A12, A14;
:: thesis: verum
end; thus
R is
auxiliary(iv)
:: thesis: verum end;
then reconsider R =
R as
auxiliary Relation of
L ;
A18:
for
x,
y being
set holds
(
[x,y] in R iff ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = x &
y' = y &
s' = a &
x' in s' . y' ) )
by A3;
take b =
R;
:: thesis: ( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
b in Aux L
by Def9;
hence
(
b in the
carrier of
(InclPoset (Aux L)) &
S1[
a,
b] )
by A18, YELLOW_1:1;
:: thesis: verum
end;
consider f being Function of the carrier of (MonSet L),the carrier of (InclPoset (Aux L)) such that
A19:
for a being set st a in the carrier of (MonSet L) holds
S1[a,f . a]
from FUNCT_2:sch 1(A1);
reconsider f' = f as Function of (MonSet L),(InclPoset (Aux L)) ;
take
f'
; :: thesis: for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = f' . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) )
let s be set ; :: thesis: ( s in the carrier of (MonSet L) implies ex AR being auxiliary Relation of L st
( AR = f' . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) )
assume A20:
s in the carrier of (MonSet L)
; :: thesis: ex AR being auxiliary Relation of L st
( AR = f' . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) )
then reconsider s' = s as Element of (MonSet L) ;
f' . s' in the carrier of (InclPoset (Aux L))
;
then
f' . s' in Aux L
by YELLOW_1:1;
then reconsider fs = f' . s' as auxiliary Relation of L by Def9;
take
fs
; :: thesis: ( fs = f' . s & ( for x, y being set holds
( [x,y] in fs iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) )
ex AR being auxiliary Relation of L st
( AR = f' . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) )
by A19, A20;
hence
( fs = f' . s & ( for x, y being set holds
( [x,y] in fs iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) )
; :: thesis: verum