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 & 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
A4: ( s <= sup D & X misses D ) by A3;
consider E being non empty directed Subset of N such that
A5: ( s <= sup E & Y misses E ) by A3;
consider xy being Element of N such that
A6: ( s = xy & ( for D being non empty directed Subset of N st xy <= sup D holds
X \/ Y meets D ) ) by A1;
s "/\" s = s by YELLOW_0:25;
then s <= (sup D) "/\" (sup E) by A4, A5, YELLOW_3:2;
then s <= sup (D "/\" E) by WAYBEL_2:51;
then X \/ Y meets D "/\" E by A6;
then A7: (X \/ Y) /\ (D "/\" E) <> {} by XBOOLE_0:def 7;
( X misses D "/\" E & Y misses D "/\" E ) by A4, A5, YELLOW12:21;
then ( X /\ (D "/\" E) = {} & Y /\ (D "/\" E) = {} ) by XBOOLE_0:def 7;
then (X /\ (D "/\" E)) \/ (Y /\ (D "/\" E)) = {} ;
hence contradiction by A7, XBOOLE_1:23; :: thesis: verum