let L be non empty complete Poset; 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; 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; ( "/\" (X,L) in the carrier of S implies "/\" (X,S) = "/\" (X,L) )
assume A1:
"/\" (X,L) in the carrier of S
; "/\" (X,S) = "/\" (X,L)
ex_inf_of X,L
by Th17;
hence
"/\" (X,S) = "/\" (X,L)
by A1, Th63; verum