let L be non empty complete Poset; :: thesis: for S being non empty full SubRelStr of L
for X being Subset of S st "/\" (X,L) in the carrier of S holds
"/\" (X,S) = "/\" (X,L)
let S be non empty full SubRelStr of L; :: thesis: for X being Subset of S st "/\" (X,L) in the carrier of S holds
"/\" (X,S) = "/\" (X,L)
let X be Subset of S; :: thesis: ( "/\" (X,L) in the carrier of S implies "/\" (X,S) = "/\" (X,L) )
assume A1: "/\" (X,L) in the carrier of S ; :: thesis: "/\" (X,S) = "/\" (X,L)
ex_inf_of X,L by Th17;
hence "/\" (X,S) = "/\" (X,L) by A1, Th63; :: thesis: verum