set B = ].-infty,1.[;
set C = RAT (2,4);
take R^1 ; :: thesis: ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict )
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 C = [.2,4.] by BORSUK_5:54;
Cl B = ].-infty,1.] by BORSUK_5:77;
then Cl A = ].-infty,1.] \/ [.2,4.] by A2, PRE_TOPC:50;
then A3: Int (Cl A) = ].-infty,1.[ \/ ].2,4.[ by Th44;
A4: Cl (Int A) = ].-infty,1.] by Th37, BORSUK_5:77;
3 in ].2,4.[ by XXREAL_1:4;
then 3 in Int (Cl A) by A3, XBOOLE_0:def 3;
then A5: not Int (Cl A) c= Cl (Int A) by A4, XXREAL_1:234;
A6: not 1 in ].2,4.[ by XXREAL_1:4;
A7: not 1 in ].-infty,1.[ by XXREAL_1:4;
1 in Cl (Int A) by A4, XXREAL_1:234;
then not Cl (Int A) c= Int (Cl A) by A3, A7, 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