let L be non empty RelStr ; for S1, S2 being meet-closed Subset of L holds S1 /\ S2 is meet-closed
let S1, S2 be meet-closed Subset of L; S1 /\ S2 is meet-closed
A1:
subrelstr S2 is meet-inheriting
by Def1;
A2:
subrelstr S1 is meet-inheriting
by Def1;
now for x, y being Element of L st x in the carrier of (subrelstr (S1 /\ S2)) & y in the carrier of (subrelstr (S1 /\ S2)) & ex_inf_of {x,y},L holds
inf {x,y} in the carrier of (subrelstr (S1 /\ S2))let x,
y be
Element of
L;
( x in the carrier of (subrelstr (S1 /\ S2)) & y in the carrier of (subrelstr (S1 /\ S2)) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (subrelstr (S1 /\ S2)) )assume that A3:
x in the
carrier of
(subrelstr (S1 /\ S2))
and A4:
y in the
carrier of
(subrelstr (S1 /\ S2))
and A5:
ex_inf_of {x,y},
L
;
inf {x,y} in the carrier of (subrelstr (S1 /\ S2))A6:
y in S1 /\ S2
by A4, YELLOW_0:def 15;
then
y in S2
by XBOOLE_0:def 4;
then A7:
y in the
carrier of
(subrelstr S2)
by YELLOW_0:def 15;
A8:
x in S1 /\ S2
by A3, YELLOW_0:def 15;
then
x in S2
by XBOOLE_0:def 4;
then
x in the
carrier of
(subrelstr S2)
by YELLOW_0:def 15;
then
inf {x,y} in the
carrier of
(subrelstr S2)
by A1, A5, A7, YELLOW_0:def 16;
then A9:
inf {x,y} in S2
by YELLOW_0:def 15;
y in S1
by A6, XBOOLE_0:def 4;
then A10:
y in the
carrier of
(subrelstr S1)
by YELLOW_0:def 15;
x in S1
by A8, XBOOLE_0:def 4;
then
x in the
carrier of
(subrelstr S1)
by YELLOW_0:def 15;
then
inf {x,y} in the
carrier of
(subrelstr S1)
by A2, A5, A10, YELLOW_0:def 16;
then
inf {x,y} in S1
by YELLOW_0:def 15;
then
inf {x,y} in S1 /\ S2
by A9, XBOOLE_0:def 4;
hence
inf {x,y} in the
carrier of
(subrelstr (S1 /\ S2))
by YELLOW_0:def 15;
verum end;
then
subrelstr (S1 /\ S2) is meet-inheriting
by YELLOW_0:def 16;
hence
S1 /\ S2 is meet-closed
by Def1; verum