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:
defpred S1[ 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 b1 being Element of the carrier of L st
( b1 in fininfs B & b1 <= a ) )

assume a in fininfs A ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in fininfs B & b1 <= 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 & S1[e,u] )
proof
let e be object ; :: thesis: ( e in Y implies ex u being object st
( u in B & S1[e,u] ) )

assume A5: e in Y ; :: thesis: ex u being object st
( u in B & S1[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 & S1[e,u] ) ; :: thesis: verum
end;
consider f being Function of Y,B such that
A6: for e being object st e in Y holds
S1[e,f . e] from 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 ;
hence y in the carrier of L by A9; :: thesis: verum
end;
A10: now :: thesis: ( ( Y = {} & ex_inf_of f .: Y,L ) or ( Y <> {} & ex_inf_of f .: Y,L ) )
per cases ( Y = {} or Y <> {} ) ;
case Y <> {} ; :: thesis: ex_inf_of f .: Y,L
then consider e being object such that
A11: e in Y by XBOOLE_0:def 1;
dom f = Y by FUNCT_2:def 1;
then f . e in f .: Y by ;
hence ex_inf_of f .: Y,L by ; :: thesis: verum
end;
end;
end;
"/\" ((f .: Y),L) is_<=_than Y
proof
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 ;
then "/\" ((f .: Y),L) <= y by ;
hence "/\" ((f .: Y),L) <= e by ; :: thesis: verum
end;
then A16: "/\" ((f .: Y),L) <= "/\" (Y,L) by ;
"/\" ((f .: Y),L) in fininfs B by A10;
hence ex b being Element of L st
( b in fininfs B & b <= a ) by ; :: thesis: verum