let x be object ; :: thesis: for Y being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) )
let Y be set ; :: thesis: ( Y c= {x} iff ( Y = {} or Y = {x} ) )
thus ( not Y c= {x} or Y = {} or Y = {x} ) :: thesis: ( ( Y = {} or Y = {x} ) implies Y c= {x} )

proof

assume A1: Y c= {x} ; :: thesis: ( Y = {} or Y = {x} )
( x in Y or not x in Y ) ;
then ( {x} c= Y or Y c= {x} \ {x} ) by A1, Lm1, Lm2;
then ( {x} = Y or Y c= {} ) by A1, XBOOLE_1:37;
hence ( Y = {} or Y = {x} ) by XBOOLE_1:3; :: thesis: verum

end;

thus ( ( Y = {} or Y = {x} ) implies Y c= {x} ) ; :: thesis: verum