let L be Semilattice; :: thesis: for A being Subset of L

for B being non empty Subset of L st A is_coarser_than B holds

fininfs A is_coarser_than fininfs B

let A be Subset of L; :: thesis: for B being non empty Subset of L st A is_coarser_than B holds

fininfs A is_coarser_than fininfs B

let B be non empty Subset of L; :: thesis: ( A is_coarser_than B implies fininfs A is_coarser_than fininfs B )

assume A1: for a being Element of L st a in A holds

ex b being Element of L st

( b in B & b <= a ) ; :: according to YELLOW_4:def 2 :: thesis: fininfs A is_coarser_than fininfs B

defpred S_{1}[ object , object ] means ex x, y being Element of L st

( x = $1 & y = $2 & y <= x );

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in fininfs A or ex b_{1} being Element of the carrier of L st

( b_{1} in fininfs B & b_{1} <= a ) )

assume a in fininfs A ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in fininfs B & b_{1} <= a )

then consider Y being finite Subset of A such that

A2: a = "/\" (Y,L) and

A3: ex_inf_of Y,L ;

A4: for e being object st e in Y holds

ex u being object st

( u in B & S_{1}[e,u] )

A6: for e being object st e in Y holds

S_{1}[e,f . e]
from FUNCT_2:sch 1(A4);

A7: f .: Y c= the carrier of L

"/\" ((f .: Y),L) in fininfs B by A10;

hence ex b being Element of L st

( b in fininfs B & b <= a ) by A2, A16; :: thesis: verum

for B being non empty Subset of L st A is_coarser_than B holds

fininfs A is_coarser_than fininfs B

let A be Subset of L; :: thesis: for B being non empty Subset of L st A is_coarser_than B holds

fininfs A is_coarser_than fininfs B

let B be non empty Subset of L; :: thesis: ( A is_coarser_than B implies fininfs A is_coarser_than fininfs B )

assume A1: for a being Element of L st a in A holds

ex b being Element of L st

( b in B & b <= a ) ; :: according to YELLOW_4:def 2 :: thesis: fininfs A is_coarser_than fininfs B

defpred S

( x = $1 & y = $2 & y <= x );

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in fininfs A or ex b

( b

assume a in fininfs A ; :: thesis: ex b

( b

then consider Y being finite Subset of A such that

A2: a = "/\" (Y,L) and

A3: ex_inf_of Y,L ;

A4: for e being object st e in Y holds

ex u being object st

( u in B & S

proof

consider f being Function of Y,B such that
let e be object ; :: thesis: ( e in Y implies ex u being object st

( u in B & S_{1}[e,u] ) )

assume A5: e in Y ; :: thesis: ex u being object st

( u in B & S_{1}[e,u] )

Y c= the carrier of L by XBOOLE_1:1;

then reconsider e = e as Element of L by A5;

ex b being Element of L st

( b in B & b <= e ) by A1, A5;

hence ex u being object st

( u in B & S_{1}[e,u] )
; :: thesis: verum

end;( u in B & S

assume A5: e in Y ; :: thesis: ex u being object st

( u in B & S

Y c= the carrier of L by XBOOLE_1:1;

then reconsider e = e as Element of L by A5;

ex b being Element of L st

( b in B & b <= e ) by A1, A5;

hence ex u being object st

( u in B & S

A6: for e being object st e in Y holds

S

A7: f .: Y c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: Y or y in the carrier of L )

assume y in f .: Y ; :: thesis: y in the carrier of L

then consider x being object such that

A8: x in dom f and

x in Y and

A9: y = f . x by FUNCT_1:def 6;

f . x in B by A8, FUNCT_2:5;

hence y in the carrier of L by A9; :: thesis: verum

end;assume y in f .: Y ; :: thesis: y in the carrier of L

then consider x being object such that

A8: x in dom f and

x in Y and

A9: y = f . x by FUNCT_1:def 6;

f . x in B by A8, FUNCT_2:5;

hence y in the carrier of L by A9; :: thesis: verum

A10: now :: thesis: ( ( Y = {} & ex_inf_of f .: Y,L ) or ( Y <> {} & ex_inf_of f .: Y,L ) )

"/\" ((f .: Y),L) is_<=_than Y
end;

proof

then A16:
"/\" ((f .: Y),L) <= "/\" (Y,L)
by A3, YELLOW_0:31;
let e be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not e in Y or "/\" ((f .: Y),L) <= e )

assume A12: e in Y ; :: thesis: "/\" ((f .: Y),L) <= e

then consider x, y being Element of L such that

A13: x = e and

A14: y = f . e and

A15: y <= x by A6;

dom f = Y by FUNCT_2:def 1;

then f . e in f .: Y by A12, FUNCT_1:def 6;

then "/\" ((f .: Y),L) <= y by A10, A14, YELLOW_4:2;

hence "/\" ((f .: Y),L) <= e by A13, A15, ORDERS_2:3; :: thesis: verum

end;assume A12: e in Y ; :: thesis: "/\" ((f .: Y),L) <= e

then consider x, y being Element of L such that

A13: x = e and

A14: y = f . e and

A15: y <= x by A6;

dom f = Y by FUNCT_2:def 1;

then f . e in f .: Y by A12, FUNCT_1:def 6;

then "/\" ((f .: Y),L) <= y by A10, A14, YELLOW_4:2;

hence "/\" ((f .: Y),L) <= e by A13, A15, ORDERS_2:3; :: thesis: verum

"/\" ((f .: Y),L) in fininfs B by A10;

hence ex b being Element of L st

( b in fininfs B & b <= a ) by A2, A16; :: thesis: verum