let x, y be object ; :: thesis: for X being set st not x in X holds
Ext ({X},x,y) = {X}
let X be set ; :: thesis: ( not x in X implies Ext ({X},x,y) = {X} )
assume A1: not x in X ; :: thesis: Ext ({X},x,y) = {X}
thus Ext ({X},x,y) c= {X} :: according to XBOOLE_0:def 10 :: thesis: {X} 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} )
assume a in Ext ({X},x,y) ; :: thesis: a in {X}

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}

then ex A being Element of {X} st
( a = A \/ {y} & x in A ) ;
hence a in {X} by A1, 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}

then ex A being Element of {X} st
( a = A & not x in A & A in {X} ) ;
hence a in {X} ; :: thesis: verum

end;

end;

end;

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