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, Th64; :: thesis: verum