let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)
let A1 be SetSequence of X; :: thesis: A \ (lim_sup A1) c= lim_sup (A (\) A1)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ (lim_sup A1) or x in lim_sup (A (\) A1) )
assume A1: x in A \ (lim_sup A1) ; :: thesis: x in lim_sup (A (\) A1)
then not x in lim_sup A1 by XBOOLE_0:def 5;
then consider n1 being Element of NAT such that
A2: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_0:5;
assume not x in lim_sup (A (\) A1) ; :: thesis: contradiction
then consider n being Element of NAT such that
A3: for k being Element of NAT holds not x in (A (\) A1) . (n + k) by KURATO_0:5;

A4: now

let k be Element of NAT ; :: thesis: ( not x in A or x in A1 . (n + k) )
not x in (A (\) A1) . (n + k) by A3;
then not x in A \ (A1 . (n + k)) by Def7;
hence ( not x in A or x in A1 . (n + k) ) by XBOOLE_0:def 5; :: thesis: verum

end;

per cases ( not x in A or for k being Element of NAT holds x in A1 . (n + k) ) by A4;

suppose not x in A ; :: thesis: contradiction

hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A5: for k being Element of NAT holds x in A1 . (n + k) ; :: thesis: contradiction

not x in A1 . (n1 + n) by A2;
hence contradiction by A5; :: thesis: verum

end;

end;