let N be meet-continuous LATTICE; :: thesis: for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0
let X, Y be upper Subset of N; :: thesis: (X ^0) \/ (Y ^0) = (X \/ Y) ^0
thus (X ^0) \/ (Y ^0) c= (X \/ Y) ^0 by Th27; :: according to XBOOLE_0:def 10 :: thesis: (X \/ Y) ^0 c= (X ^0) \/ (Y ^0)
assume not (X \/ Y) ^0 c= (X ^0) \/ (Y ^0) ; :: thesis: contradiction
then consider s being set such that
A1: s in (X \/ Y) ^0 and
A2: not s in (X ^0) \/ (Y ^0) by TARSKI:def 3;
A3: not s in X ^0 by A2, XBOOLE_0:def 3;
A4: not s in Y ^0 by A2, XBOOLE_0:def 3;
reconsider s = s as Element of N by A1;
consider D being non empty directed Subset of N such that
A5: s <= sup D and
A6: X misses D by A3;
consider E being non empty directed Subset of N such that
A7: s <= sup E and
A8: Y misses E by A4;
s "/\" s = s by YELLOW_0:25;
then s <= (sup D) "/\" (sup E) by A5, A7, YELLOW_3:2;
then A9: s <= sup (D "/\" E) by WAYBEL_2:51;
ex xy being Element of N st
( s = xy & ( for D being non empty directed Subset of N st xy <= sup D holds
X \/ Y meets D ) ) by A1;
then X \/ Y meets D "/\" E by A9;
then A10: (X \/ Y) /\ (D "/\" E) <> {} by XBOOLE_0:def 7;
X misses D "/\" E by A6, YELLOW12:21;
then A11: X /\ (D "/\" E) = {} by XBOOLE_0:def 7;
Y misses D "/\" E by A8, YELLOW12:21;
then (X /\ (D "/\" E)) \/ (Y /\ (D "/\" E)) = {} by A11, XBOOLE_0:def 7;
hence contradiction by A10, XBOOLE_1:23; :: thesis: verum