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₁[ 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₁ being Element of the carrier of L st
( b₁ in fininfs B & b₁ <= a ) )
assume a in fininfs A ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in fininfs B & b₁ <= 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₁[e,u] )

proof

let e be object ; :: thesis: ( e in Y implies ex u being object st
( u in B & S₁[e,u] ) )
assume A5: e in Y ; :: thesis: ex u being object st
( u in B & S₁[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₁[e,u] ) ; :: thesis: verum

end;

consider f being Function of Y,B such that
A6: for e being object st e in Y holds
S₁[e,f . e] from FUNCT_2:sch 1(A4);
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;

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

hence ex_inf_of f .: Y,L by A3; :: thesis: verum

end;

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 A11, FUNCT_1:def 6;
hence ex_inf_of f .: Y,L by A7, YELLOW_0:55; :: 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 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;

then A16: "/\" ((f .: Y),L) <= "/\" (Y,L) by A3, YELLOW_0:31;
"/\" ((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