let C be non empty set ; :: thesis: for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t))
let s, t be Element of (FuzzyLattice C); :: thesis: s "/\" t = min ((@ s),(@ t))
( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ;
hence s "/\" t = min ((@ s),(@ t)) by Th20; :: thesis: verum