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

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