let L be non empty RelStr ; :: thesis: 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; :: thesis: ( 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 ) :: thesis: ( ( for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in S ) implies S is infs-closed )

"/\" (X,L) in S ; :: thesis: S is infs-closed

hence S is infs-closed ; :: thesis: verum

( 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; :: thesis: ( 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 ) :: thesis: ( ( for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in S ) implies S is infs-closed )

proof

assume A3:
for X being Subset of S st ex_inf_of X,L holds
assume
S is infs-closed
; :: thesis: for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in S

then A1: subrelstr S is infs-inheriting ;

let X be Subset of S; :: thesis: ( ex_inf_of X,L implies "/\" (X,L) in S )

assume A2: ex_inf_of X,L ; :: thesis: "/\" (X,L) in S

X is Subset of (subrelstr S) by YELLOW_0:def 15;

then "/\" (X,L) in the carrier of (subrelstr S) by A1, A2;

hence "/\" (X,L) in S by YELLOW_0:def 15; :: thesis: verum

end;"/\" (X,L) in S

then A1: subrelstr S is infs-inheriting ;

let X be Subset of S; :: thesis: ( ex_inf_of X,L implies "/\" (X,L) in S )

assume A2: ex_inf_of X,L ; :: thesis: "/\" (X,L) in S

X is Subset of (subrelstr S) by YELLOW_0:def 15;

then "/\" (X,L) in the carrier of (subrelstr S) by A1, A2;

hence "/\" (X,L) in S by YELLOW_0:def 15; :: thesis: verum

"/\" (X,L) in S ; :: thesis: S is infs-closed

now :: thesis: for X being Subset of (subrelstr S) st ex_inf_of X,L holds

"/\" (X,L) in the carrier of (subrelstr S)

then
subrelstr S is infs-inheriting
;"/\" (X,L) in the carrier of (subrelstr S)

let X be Subset of (subrelstr S); :: thesis: ( ex_inf_of X,L implies "/\" (X,L) in the carrier of (subrelstr S) )

assume A4: ex_inf_of X,L ; :: thesis: "/\" (X,L) in the carrier of (subrelstr S)

X is Subset of S by YELLOW_0:def 15;

then "/\" (X,L) in S by A3, A4;

hence "/\" (X,L) in the carrier of (subrelstr S) by YELLOW_0:def 15; :: thesis: verum

end;assume A4: ex_inf_of X,L ; :: thesis: "/\" (X,L) in the carrier of (subrelstr S)

X is Subset of S by YELLOW_0:def 15;

then "/\" (X,L) in S by A3, A4;

hence "/\" (X,L) in the carrier of (subrelstr S) by YELLOW_0:def 15; :: thesis: verum

hence S is infs-closed ; :: thesis: verum