thus weight Sorgenfrey-line c= continuum by Lm5, Lm6, Th20, WAYBEL23:73; :: according to XBOOLE_0:def 10 :: thesis: continuum c= weight Sorgenfrey-line
consider B being Basis of Sorgenfrey-line such that
A1: weight Sorgenfrey-line = card B by WAYBEL23:74;
assume not continuum c= weight Sorgenfrey-line ; :: thesis: contradiction
then A2: weight Sorgenfrey-line in continuum by CARD_1:4;
the carrier of Sorgenfrey-line = REAL by Def2;
then consider x being Real, q being Rational such that
x < q and
A3: not [.x,q.[ in UniCl B by A2, A1, Th32;
[.x,q.[ is open Subset of Sorgenfrey-line by Th11;
then [.x,q.[ in the topology of Sorgenfrey-line by PRE_TOPC:def 2;
hence contradiction by A3, YELLOW_9:22; :: thesis: verum