let L be non empty transitive RelStr ; :: thesis: for S being non empty infs-closed Subset of L
for X being Subset of S st ex_inf_of X,L holds
( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
let S be non empty infs-closed Subset of L; :: thesis: for X being Subset of S st ex_inf_of X,L holds
( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
let X be Subset of S; :: thesis: ( ex_inf_of X,L implies ( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) ) )
A1: X is Subset of (subrelstr S) by YELLOW_0:def 15;
assume A2: ex_inf_of X,L ; :: thesis: ( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
subrelstr S is non empty full infs-inheriting SubRelStr of L by Def3;
then "/\" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def 18;
hence ( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) ) by A1, A2, YELLOW_0:63; :: thesis: verum