let L be non empty RelStr ; for S being Subset of L holds
( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
let S be Subset of L; ( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
thus
( S is infs-closed implies for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
( ( for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S ) implies S is infs-closed )
assume A3:
for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S
; S is infs-closed
then
subrelstr S is infs-inheriting
;
hence
S is infs-closed
; verum