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:17;
A2: Cl C = [.2,4.] by BORSUK_5:31;
Cl B = ].-infty,1.] by BORSUK_5:51;
then Cl A = ].-infty,1.] \/ [.2,4.] by A2, PRE_TOPC:20;
then A3: Int (Cl A) = ].-infty,1.[ \/ ].2,4.[ by Th34;
A4: Cl (Int A) = ].-infty,1.] by Th32, BORSUK_5:51;
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 ;
hence ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict ) ; :: thesis: verum