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
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 A2: a in fininfs A ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in fininfs B & b₁ <= a )
consider Y being finite Subset of A such that
A3: a = "/\" Y,L and
A4: ex_inf_of Y,L by A2;
defpred S₁[ set , set ] means ex x, y being Element of L st
( x = $1 & y = $2 & y <= x );
A5: for e being set st e in Y holds
ex u being set st
( u in B & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in Y implies ex u being set st
( u in B & S₁[e,u] ) )
assume A6: e in Y ; :: thesis: ex u being set 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 A6;
ex b being Element of L st
( b in B & b <= e ) by A1, A6;
hence ex u being set st
( u in B & S₁[e,u] ) ; :: thesis: verum

end;

consider f being Function of Y,B such that
A7: for e being set st e in Y holds
S₁[e,f . e] from FUNCT_2:sch 1(A5);
A8: f .: Y c= the carrier of L

proof

let y be set ; :: 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 set such that
A9: ( x in dom f & x in Y & y = f . x ) by FUNCT_1:def 12;
f . x in B by A9, FUNCT_2:7;
hence y in the carrier of L by A9; :: thesis: verum

end;

A10: now

per cases ( Y = {} or Y <> {} ) ;

case Y = {} ; :: thesis: ex_inf_of f .: Y,L

hence ex_inf_of f .: Y,L by A4, RELAT_1:149; :: thesis: verum

end;

case Y <> {} ; :: thesis: ex_inf_of f .: Y,L

then consider e being set 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 12;
hence ex_inf_of f .: Y,L by A8, YELLOW_0:55; :: thesis: verum

end;

end;

end;

then A12: "/\" (f .: Y),L in fininfs B ;
"/\" (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 A13: e in Y ; :: thesis: "/\" (f .: Y),L <= e
then consider x, y being Element of L such that
A14: ( x = e & y = f . e & y <= x ) by A7;
dom f = Y by FUNCT_2:def 1;
then f . e in f .: Y by A13, FUNCT_1:def 12;
then "/\" (f .: Y),L <= y by A10, A14, YELLOW_4:2;
hence "/\" (f .: Y),L <= e by A14, ORDERS_2:26; :: thesis: verum

end;

then "/\" (f .: Y),L <= "/\" Y,L by A4, YELLOW_0:31;
hence ex b being Element of L st
( b in fininfs B & b <= a ) by A3, A12; :: thesis: verum