let x, y be object ; :: thesis: for X being set st x in X holds
Ext ({X},x,y) = {(X \/ {y})}
let X be set ; :: thesis: ( x in X implies Ext ({X},x,y) = {(X \/ {y})} )
assume A1: x in X ; :: thesis: Ext ({X},x,y) = {(X \/ {y})}
thus Ext ({X},x,y) c= {(X \/ {y})} :: according to XBOOLE_0:def 10 :: thesis: {(X \/ {y})} c= Ext ({X},x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ext ({X},x,y) or a in {(X \/ {y})} )
assume a in Ext ({X},x,y) ; :: thesis: a in {(X \/ {y})}

per cases then ( a in { (A \/ {y}) where A is Element of {X} : x in A } or a in { A where A is Element of {X} : ( not x in A & A in {X} ) } ) by XBOOLE_0:def 3;

suppose a in { (A \/ {y}) where A is Element of {X} : x in A } ; :: thesis: a in {(X \/ {y})}

then consider A being Element of {X} such that
A2: ( a = A \/ {y} & x in A ) ;
A = X by TARSKI:def 1;
hence a in {(X \/ {y})} by A2, TARSKI:def 1; :: thesis: verum

end;

suppose a in { A where A is Element of {X} : ( not x in A & A in {X} ) } ; :: thesis: a in {(X \/ {y})}

then ex A being Element of {X} st
( a = A & not x in A & A in {X} ) ;
hence a in {(X \/ {y})} by A1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(X \/ {y})} or a in Ext ({X},x,y) )
assume a in {(X \/ {y})} ; :: thesis: a in Ext ({X},x,y)
then ( a = X \/ {y} & X in {X} ) by TARSKI:def 1;
then a in { (A \/ {y}) where A is Element of {X} : x in A } by A1;
hence a in Ext ({X},x,y) by XBOOLE_0:def 3; :: thesis: verum