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 S2 is join-inheriting by Def2;

A2: subrelstr S1 is join-inheriting by Def2;

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

let S1, S2 be join-closed Subset of L; :: thesis: S1 /\ S2 is join-closed

A1: subrelstr S2 is join-inheriting by Def2;

A2: subrelstr S1 is join-inheriting by Def2;

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_sup_of {x,y},L holds

sup {x,y} in the carrier of (subrelstr (S1 /\ S2))

then
subrelstr (S1 /\ S2) is join-inheriting
;sup {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_sup_of {x,y},L implies sup {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_sup_of {x,y},L ; :: thesis: sup {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 sup {x,y} in the carrier of (subrelstr S2) by A1, A5, A7;

then A9: sup {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 sup {x,y} in the carrier of (subrelstr S1) by A2, A5, A10;

then sup {x,y} in S1 by YELLOW_0:def 15;

then sup {x,y} in S1 /\ S2 by A9, XBOOLE_0:def 4;

hence sup {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_sup_of {x,y},L ; :: thesis: sup {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 sup {x,y} in the carrier of (subrelstr S2) by A1, A5, A7;

then A9: sup {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 sup {x,y} in the carrier of (subrelstr S1) by A2, A5, A10;

then sup {x,y} in S1 by YELLOW_0:def 15;

then sup {x,y} in S1 /\ S2 by A9, XBOOLE_0:def 4;

hence sup {x,y} in the carrier of (subrelstr (S1 /\ S2)) by YELLOW_0:def 15; :: thesis: verum

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