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;

hence S1 /\ S2 is meet-closed ; :: thesis: verum

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))

then
subrelstr (S1 /\ S2) is meet-inheriting
;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 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;

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;

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; :: thesis: verum

end;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 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;

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;

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; :: thesis: verum

hence S1 /\ S2 is meet-closed ; :: thesis: verum