the topology of Sierpinski_Space = {{} ,{1},{0 ,1}} by WAYBEL18:def 9;
then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;
then reconsider A = {1} as open Subset of by PRE_TOPC:def 5;
consider f being Function of (InclPoset the topology of X),(oContMaps X,Sierpinski_Space ) such that
A1: f is isomorphic and
A2: for V being open Subset of holds f . V = chi V,the carrier of X by WAYBEL26:5;
rng f = [#] (oContMaps X,Sierpinski_Space ) by A1, WAYBEL_0:66;
then A3: f " = f " by A1, TOPS_2:def 4;
A4: the carrier of (InclPoset the topology of X) = the topology of X by YELLOW_1:1;
A5: the carrier of Sierpinski_Space = {0 ,1} by WAYBEL18:def 9;

now

let x be Element of ; :: thesis: (alpha X) . x = (f " ) . x
reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2;
[#] Sierpinski_Space <> {} ;
then A6: g " A is open by TOPS_2:55;
then A7: g " A in the topology of X by PRE_TOPC:def 5;
A8: f . (g " A) = chi (g " A),the carrier of X by A2, A6
.= x by A5, FUNCT_3:49 ;
thus (alpha X) . x = g " A by Def4
.= (f " ) . x by A1, A3, A4, A7, A8, FUNCT_2:32 ; :: thesis: verum

end;

hence alpha X is isomorphic by A1, A3, FUNCT_2:113, WAYBEL_0:68; :: thesis: verum