let L be non empty RelStr ; :: thesis: for S1, S2 being join-closed Subset of L holds S1 /\ S2 is join-closed
let S1, S2 be join-closed Subset of L; :: thesis: S1 /\ S2 is join-closed
A1:
( subrelstr S1 is join-inheriting & subrelstr S2 is join-inheriting )
by Def2;
now let x,
y be
Element of
L;
:: thesis: ( x in the carrier of (subrelstr (S1 /\ S2)) & y in the carrier of (subrelstr (S1 /\ S2)) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (subrelstr (S1 /\ S2)) )assume that A2:
x in the
carrier of
(subrelstr (S1 /\ S2))
and A3:
y in the
carrier of
(subrelstr (S1 /\ S2))
and A4:
ex_sup_of {x,y},
L
;
:: thesis: sup {x,y} in the carrier of (subrelstr (S1 /\ S2))
(
x in S1 /\ S2 &
y in S1 /\ S2 )
by A2, A3, YELLOW_0:def 15;
then
(
x in S1 &
x in S2 &
y in S1 &
y in S2 )
by XBOOLE_0:def 4;
then
(
x in the
carrier of
(subrelstr S1) &
x in the
carrier of
(subrelstr S2) &
y in the
carrier of
(subrelstr S1) &
y in the
carrier of
(subrelstr S2) )
by YELLOW_0:def 15;
then
(
sup {x,y} in the
carrier of
(subrelstr S1) &
sup {x,y} in the
carrier of
(subrelstr S2) )
by A1, A4, YELLOW_0:def 17;
then
(
sup {x,y} in S1 &
sup {x,y} in S2 )
by YELLOW_0:def 15;
then
sup {x,y} in S1 /\ S2
by XBOOLE_0:def 4;
hence
sup {x,y} in the
carrier of
(subrelstr (S1 /\ S2))
by YELLOW_0:def 15;
:: thesis: verum end;
then
subrelstr (S1 /\ S2) is join-inheriting
by YELLOW_0:def 17;
hence
S1 /\ S2 is join-closed
by Def2; :: thesis: verum