let R be /\-complete Semilattice; :: thesis: for S being Subset of R
for a being Element of R st a in S holds
"/\" (S,R) <= a
let S be Subset of R; :: thesis: for a being Element of R st a in S holds
"/\" (S,R) <= a
let a be Element of R; :: 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; :: thesis: verum