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 object ; :: 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 ;

let X, Y be Subset of N; :: thesis: (X ^0) \/ (Y ^0) c= (X \/ Y) ^0

let a be object ; :: 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 :: thesis: for D being non empty directed Subset of N st b <= sup D holds

X \/ Y meets D

hence
a in (X \/ Y) ^0
; :: thesis: verumX \/ Y meets D

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

end;assume A2: b <= sup D ; :: thesis: X \/ Y meets D

now :: thesis: (X \/ Y) /\ D <> {} end;

hence
X \/ Y meets D
; :: thesis: verumper cases
( a in X ^0 or a in Y ^0 )
by A1, XBOOLE_0:def 3;

end;

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

then
ex x being Element of N st

( a = x & ( for D being non empty directed Subset of N st x <= sup D holds

X meets D ) ) ;

then X meets D by A2;

then X /\ D <> {} ;

then (X /\ D) \/ (Y /\ D) <> {} ;

hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; :: thesis: verum

end;( a = x & ( for D being non empty directed Subset of N st x <= sup D holds

X meets D ) ) ;

then X meets D by A2;

then X /\ D <> {} ;

then (X /\ D) \/ (Y /\ D) <> {} ;

hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; :: thesis: verum

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

then
ex y being Element of N st

( a = y & ( for D being non empty directed Subset of N st y <= sup D holds

Y meets D ) ) ;

then Y meets D by A2;

then Y /\ D <> {} ;

then (X /\ D) \/ (Y /\ D) <> {} ;

hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; :: thesis: verum

end;( a = y & ( for D being non empty directed Subset of N st y <= sup D holds

Y meets D ) ) ;

then Y meets D by A2;

then Y /\ D <> {} ;

then (X /\ D) \/ (Y /\ D) <> {} ;

hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; :: thesis: verum