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:49, TOPS_1:44;
then Int (Cl (Int B)) c= Int (Cl B) by TOPS_1:48;
then Cl (Int (Cl (Int B))) c= Cl (Int (Cl B)) by PRE_TOPC:49;
then Cl (Int B) c= Cl (Int (Cl B)) by TOPS_1:58;
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:49, XBOOLE_1:17;
then A2: Cl (B /\ (Int (Cl B))) c= Cl (Int B) by TOPS_1:58;
Cl (B /\ (Int (Cl B))) = Cl ((Cl B) /\ (Int (Cl B))) by TOPS_1:41;
then Cl (B /\ (Int (Cl B))) = Cl (Int (Cl B)) by TOPS_1:44, 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, XBOOLE_0:def 10; :: thesis: verum

end;

A3: Int (Cl B) c= Cl (Int (Cl B)) by PRE_TOPC:48;
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:48, XBOOLE_1:26;
then B /\ (Int (Cl B)) c= Cl (Int B) by A4, XBOOLE_1:1;
then A5: Cl (B /\ (Int (Cl B))) c= Cl (Cl (Int B)) by PRE_TOPC:49;
Cl (B /\ (Int (Cl B))) = Cl ((Cl B) /\ (Int (Cl B))) by TOPS_1:41;
then Cl (Int (Cl B)) c= Cl (Int B) by A5, TOPS_1:44, XBOOLE_1:28;
then Int (Cl B) c= Cl (Int B) by A3, XBOOLE_1:1;
then Int (Int (Cl B)) c= Int (Cl (Int B)) by TOPS_1:48;
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:49, TOPS_1:44;
then Int (Cl (Int B)) c= Int (Cl B) by TOPS_1:48;
then alphaInt B c= B /\ (Int (Cl B)) by XBOOLE_1:26;
hence alphaInt B = pInt B by A6, XBOOLE_0:def 10; :: thesis: verum