let N be non empty reflexive RelStr ; :: thesis: for X, Y being Subset of N holds (X ^0 ) \/ (Y ^0 ) c= (X \/ Y) ^0
let X, Y be Subset of N; :: thesis: (X ^0 ) \/ (Y ^0 ) c= (X \/ Y) ^0
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (X ^0 ) \/ (Y ^0 ) or a in (X \/ Y) ^0 )
assume A1: a in (X ^0 ) \/ (Y ^0 ) ; :: thesis: a in (X \/ Y) ^0
then reconsider b = a as Element of N ;

now

let D be non empty directed Subset of N; :: thesis: ( b <= sup D implies X \/ Y meets D )
assume A2: b <= sup D ; :: thesis: X \/ Y meets D

now

per cases ( a in X ^0 or a in Y ^0 ) by A1, XBOOLE_0:def 3;

suppose a in X ^0 ; :: thesis: (X \/ Y) /\ D <> {}

then consider x being Element of N such that
A3: ( a = x & ( for D being non empty directed Subset of N st x <= sup D holds
X meets D ) ) ;
X meets D by A2, A3;
then X /\ D <> {} by XBOOLE_0:def 7;
then (X /\ D) \/ (Y /\ D) <> {} ;
hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; :: thesis: verum

end;

suppose a in Y ^0 ; :: thesis: (X \/ Y) /\ D <> {}

then consider y being Element of N such that
A4: ( a = y & ( for D being non empty directed Subset of N st y <= sup D holds
Y meets D ) ) ;
Y meets D by A2, A4;
then Y /\ D <> {} by XBOOLE_0:def 7;
then (X /\ D) \/ (Y /\ D) <> {} ;
hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; :: thesis: verum

end;

end;

end;

hence X \/ Y meets D by XBOOLE_0:def 7; :: thesis: verum

end;

hence a in (X \/ Y) ^0 ; :: thesis: verum