let R be /\-complete Semilattice; :: thesis: for S being Subset of
for a being Element of st a in S holds
"/\" S,R <= a
let S be Subset of ; :: thesis: for a being Element of st a in S holds
"/\" S,R <= a
let a be Element of ; :: thesis: ( a in S implies "/\" S,R <= a )
assume A1: a in S ; :: thesis: "/\" S,R <= a
then ex_inf_of S,R by WAYBEL_0:76;
then S is_>=_than "/\" S,R by YELLOW_0:31;
hence "/\" S,R <= a by A1, LATTICE3:def 8; :: thesis: verum