let L be non empty transitive RelStr ; for S being non empty full filtered-infs-inheriting SubRelStr of L
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
let S be non empty full filtered-infs-inheriting SubRelStr of L; for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
let X be filtered Subset of S; ( X <> {} & ex_inf_of X,L implies ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) )
assume that
A1:
X <> {}
and
A2:
ex_inf_of X,L
; ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
"/\" (X,L) in the carrier of S
by A1, A2, Def3;
hence
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
by A2, YELLOW_0:63; verum