let L be non empty RelStr ; for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
let S be Subset of L; ( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
thus
( S is meet-closed implies for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
( ( for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S ) implies S is meet-closed )proof
assume
S is
meet-closed
;
for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S
then A1:
subrelstr S is
meet-inheriting
;
let x,
y be
Element of
L;
( x in S & y in S & ex_inf_of {x,y},L implies inf {x,y} in S )
assume that A2:
x in S
and A3:
y in S
and A4:
ex_inf_of {x,y},
L
;
inf {x,y} in S
the
carrier of
(subrelstr S) = S
by YELLOW_0:def 15;
hence
inf {x,y} in S
by A1, A2, A3, A4;
verum
end;
assume A5:
for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S
; S is meet-closed
now for x, y being Element of L st x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_inf_of {x,y},L holds
inf {x,y} in the carrier of (subrelstr S)let x,
y be
Element of
L;
( x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (subrelstr S) )assume that A6:
x in the
carrier of
(subrelstr S)
and A7:
y in the
carrier of
(subrelstr S)
and A8:
ex_inf_of {x,y},
L
;
inf {x,y} in the carrier of (subrelstr S)
the
carrier of
(subrelstr S) = S
by YELLOW_0:def 15;
hence
inf {x,y} in the
carrier of
(subrelstr S)
by A5, A6, A7, A8;
verum end;
then
subrelstr S is meet-inheriting
;
hence
S is meet-closed
; verum