let A be set ; :: thesis: for s being Subset of A
for n being set st n in A holds
s \/ {n} is Subset of A
let s be Subset of A; :: thesis: for n being set st n in A holds
s \/ {n} is Subset of A
let n be set ; :: thesis: ( n in A implies s \/ {n} is Subset of A )
assume A1: n in A ; :: thesis: s \/ {n} is Subset of A
s \/ {n} c= A

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in s \/ {n} or m in A )
assume A2: m in s \/ {n} ; :: thesis: m in A

now :: thesis: m in A

per cases ( m in s or m in {n} ) by A2, XBOOLE_0:def 3;

suppose m in s ; :: thesis: m in A

hence m in A ; :: thesis: verum

end;

suppose m in {n} ; :: thesis: m in A

hence m in A by A1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence m in A ; :: thesis: verum

end;

hence s \/ {n} is Subset of A ; :: thesis: verum