let L be non empty transitive RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( X <> {} & ex_inf_of X,L implies ( ex_inf_of X,S & "/\" X,S = "/\" X,L ) )
assume A1: ( X <> {} & ex_inf_of X,L ) ; :: thesis: ( ex_inf_of X,S & "/\" X,S = "/\" X,L )
then "/\" X,L in the carrier of S by Def3;
hence ( ex_inf_of X,S & "/\" X,S = "/\" X,L ) by A1, YELLOW_0:64; :: thesis: verum