take R^1 ; :: thesis: ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict )
set B = ].-infty ,1.[;
set C = RAT 2,4;
set A = ].-infty ,1.[ \/ (RAT 2,4);
reconsider A = ].-infty ,1.[ \/ (RAT 2,4), B = ].-infty ,1.[, C = RAT 2,4 as Subset of R^1 by TOPMETR:24;
A2: Cl (Int A) = ].-infty ,1.] by Th37, BORSUK_5:77;
A3: Cl B = ].-infty ,1.] by BORSUK_5:77;
Cl C = [.2,4.] by BORSUK_5:54;
then Cl A = ].-infty ,1.] \/ [.2,4.] by A3, PRE_TOPC:50;
then A4: Int (Cl A) = ].-infty ,1.[ \/ ].2,4.[ by Th44;
3 in ].2,4.[ by XXREAL_1:4;
then 3 in Int (Cl A) by A4, XBOOLE_0:def 3;
then A5: not Int (Cl A) c= Cl (Int A) by A2, XXREAL_1:234;
A6: 1 in Cl (Int A) by A2, XXREAL_1:234;
( not 1 in ].-infty ,1.[ & not 1 in ].2,4.[ ) by XXREAL_1:4;
then not Cl (Int A) c= Int (Cl A) by A4, A6, XBOOLE_0:def 3;
then Int (Cl A), Cl (Int A) are_c=-incomparable by A5, XBOOLE_0:def 9;
then A is 3rd_class by Def8;
hence ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict ) by Def11; :: thesis: verum