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