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 object such that

A1: s in (X \/ Y) ^0 and

A2: not s in (X ^0) \/ (Y ^0) ;

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) <> {} ;

X misses D "/\" E by A6, YELLOW12:21;

then A11: X /\ (D "/\" E) = {} ;

Y misses D "/\" E by A8, YELLOW12:21;

then (X /\ (D "/\" E)) \/ (Y /\ (D "/\" E)) = {} by A11;

hence contradiction by A10, XBOOLE_1:23; :: thesis: verum

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 object such that

A1: s in (X \/ Y) ^0 and

A2: not s in (X ^0) \/ (Y ^0) ;

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) <> {} ;

X misses D "/\" E by A6, YELLOW12:21;

then A11: X /\ (D "/\" E) = {} ;

Y misses D "/\" E by A8, YELLOW12:21;

then (X /\ (D "/\" E)) \/ (Y /\ (D "/\" E)) = {} by A11;

hence contradiction by A10, XBOOLE_1:23; :: thesis: verum