let L be non empty transitive antisymmetric complete RelStr ; :: thesis: for S being non empty infs-closed Subset of L

for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)

let S be non empty infs-closed Subset of L; :: thesis: for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)

let X be Subset of S; :: thesis: "/\" (X,(subrelstr S)) = "/\" (X,L)

ex_inf_of X,L by YELLOW_0:17;

hence "/\" (X,(subrelstr S)) = "/\" (X,L) by Th21; :: thesis: verum

for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)

let S be non empty infs-closed Subset of L; :: thesis: for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)

let X be Subset of S; :: thesis: "/\" (X,(subrelstr S)) = "/\" (X,L)

ex_inf_of X,L by YELLOW_0:17;

hence "/\" (X,(subrelstr S)) = "/\" (X,L) by Th21; :: thesis: verum