let L be non empty RelStr ; :: thesis: 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; :: thesis: ( 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 )
:: thesis: ( ( 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
;
:: thesis: 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
by Def1;
let x,
y be
Element of
L;
:: thesis: ( 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
;
:: thesis: 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, YELLOW_0:def 16;
:: thesis: 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
; :: thesis: S is meet-closed
now let x,
y be
Element of
L;
:: thesis: ( 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
;
:: thesis: 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;
:: thesis: verum end;
then
subrelstr S is meet-inheriting
by YELLOW_0:def 16;
hence
S is meet-closed
by Def1; :: thesis: verum