let T be TopSpace; :: thesis: for B being Subset of T holds
( alphaInt B = pInt B iff sInt B = psInt B )
let B be Subset of T; :: thesis: ( alphaInt B = pInt B iff sInt B = psInt B )

hereby :: thesis: ( sInt B = psInt B implies alphaInt B = pInt B )

Cl (Int B) c= Cl B by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int B)) c= Int (Cl B) by TOPS_1:19;
then Cl (Int (Cl (Int B))) c= Cl (Int (Cl B)) by PRE_TOPC:19;
then Cl (Int B) c= Cl (Int (Cl B)) by TOPS_1:26;
then A1: sInt B c= B /\ (Cl (Int (Cl B))) by XBOOLE_1:26;
assume alphaInt B = pInt B ; :: thesis: sInt B = psInt B
then Cl (B /\ (Int (Cl B))) c= Cl (Int (Cl (Int B))) by PRE_TOPC:19, XBOOLE_1:17;
then A2: Cl (B /\ (Int (Cl B))) c= Cl (Int B) by TOPS_1:26;
Cl (B /\ (Int (Cl B))) = Cl ((Cl B) /\ (Int (Cl B))) by TOPS_1:14;
then Cl (B /\ (Int (Cl B))) = Cl (Int (Cl B)) by TOPS_1:16, XBOOLE_1:28;
then B /\ (Cl (Int (Cl B))) c= B /\ (Cl (Int B)) by A2, XBOOLE_1:26;
hence sInt B = psInt B by A1; :: thesis: verum

end;

A3: Int (Cl B) c= Cl (Int (Cl B)) by PRE_TOPC:18;
assume psInt B = sInt B ; :: thesis: alphaInt B = pInt B
then A4: psInt B c= Cl (Int B) by XBOOLE_1:17;
B /\ (Int (Cl B)) c= B /\ (Cl (Int (Cl B))) by PRE_TOPC:18, XBOOLE_1:26;
then B /\ (Int (Cl B)) c= Cl (Int B) by A4;
then A5: Cl (B /\ (Int (Cl B))) c= Cl (Cl (Int B)) by PRE_TOPC:19;
Cl (B /\ (Int (Cl B))) = Cl ((Cl B) /\ (Int (Cl B))) by TOPS_1:14;
then Cl (Int (Cl B)) c= Cl (Int B) by A5, TOPS_1:16, XBOOLE_1:28;
then Int (Cl B) c= Cl (Int B) by A3;
then Int (Int (Cl B)) c= Int (Cl (Int B)) by TOPS_1:19;
then A6: B /\ (Int (Cl B)) c= B /\ (Int (Cl (Int B))) by XBOOLE_1:26;
Cl (Int B) c= Cl B by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int B)) c= Int (Cl B) by TOPS_1:19;
then alphaInt B c= B /\ (Int (Cl B)) by XBOOLE_1:26;
hence alphaInt B = pInt B by A6; :: thesis: verum