let L be non empty RelStr ; :: thesis: for S1, S2 being meet-closed Subset of L holds S1 /\ S2 is meet-closed
let S1, S2 be meet-closed Subset of L; :: thesis: S1 /\ S2 is meet-closed
A1: subrelstr S2 is meet-inheriting by Def1;
A2: subrelstr S1 is meet-inheriting by Def1;
now :: thesis: 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; :: thesis: ( 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 ; :: thesis: inf {x,y} in the carrier of (subrelstr (S1 /\ S2))
A6: y in S1 /\ S2 by ;
then y in S2 by XBOOLE_0:def 4;
then A7: y in the carrier of () by YELLOW_0:def 15;
A8: x in S1 /\ S2 by ;
then x in S2 by XBOOLE_0:def 4;
then x in the carrier of () by YELLOW_0:def 15;
then inf {x,y} in the carrier of () by A1, A5, A7;
then A9: inf {x,y} in S2 by YELLOW_0:def 15;
y in S1 by ;
then A10: y in the carrier of () by YELLOW_0:def 15;
x in S1 by ;
then x in the carrier of () by YELLOW_0:def 15;
then inf {x,y} in the carrier of () by A2, A5, A10;
then inf {x,y} in S1 by YELLOW_0:def 15;
then inf {x,y} in S1 /\ S2 by ;
hence inf {x,y} in the carrier of (subrelstr (S1 /\ S2)) by YELLOW_0:def 15; :: thesis: verum
end;
then subrelstr (S1 /\ S2) is meet-inheriting ;
hence S1 /\ S2 is meet-closed ; :: thesis: verum