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 ;
now :: thesis: for D being non empty directed Subset of N st b <= sup D holds
X \/ 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
now :: thesis: (X \/ Y) /\ D <> {}
per cases ( a in X ^0 or a in Y ^0 ) by ;
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;
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;
end;
end;
hence X \/ Y meets D ; :: thesis: verum
end;
hence a in (X \/ Y) ^0 ; :: thesis: verum