let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T being Scott TopAugmentation of L1
for B1 being Basis of T st not B1 is finite holds
not { (inf u) where u is Subset of T : u in B1 } is finite
let T be Scott TopAugmentation of L1; :: thesis: for B1 being Basis of T st not B1 is finite holds
not { (inf u) where u is Subset of T : u in B1 } is finite
let B1 be Basis of T; :: thesis: ( not B1 is finite implies not { (inf u) where u is Subset of T : u in B1 } is finite )
reconsider B2 = { (inf u) where u is Subset of T : u in B1 } as set ;
defpred S₁[ set , set ] means ex y being Element of T st
( $1 = y & $2 = wayabove y );
reconsider B3 = { (wayabove (inf u)) where u is Subset of T : u in B1 } as Basis of T by Th27;
assume that
A1: not B1 is finite and
A2: { (inf u) where u is Subset of T : u in B1 } is finite ; :: thesis: contradiction
A3: for x being set st x in B2 holds
ex y being set st
( y in B3 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in B2 implies ex y being set st
( y in B3 & S₁[x,y] ) )
assume x in B2 ; :: thesis: ex y being set st
( y in B3 & S₁[x,y] )
then A4: ex u1 being Subset of T st
( x = inf u1 & u1 in B1 ) ;
then reconsider z = x as Element of T ;
take y = wayabove z; :: thesis: ( y in B3 & S₁[x,y] )
thus y in B3 by A4; :: thesis: S₁[x,y]
take z ; :: thesis: ( x = z & y = wayabove z )
thus ( x = z & y = wayabove z ) ; :: thesis: verum

end;

consider f being Function such that
A5: dom f = B2 and
A6: rng f c= B3 and
A7: for x being set st x in B2 holds
S₁[x,f . x] from FUNCT_1:sch 5(A3);
B3 c= rng f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in B3 or z in rng f )
assume z in B3 ; :: thesis: z in rng f
then consider u1 being Subset of T such that
A8: z = wayabove (inf u1) and
A9: u1 in B1 ;
inf u1 in B2 by A9;
then A10: ex y being Element of T st
( inf u1 = y & f . (inf u1) = wayabove y ) by A7;
inf u1 in B2 by A9;
hence z in rng f by A5, A8, A10, FUNCT_1:def 3; :: thesis: verum

end;

then rng f = B3 by A6, XBOOLE_0:def 10;
then B3 is finite by A2, A5, FINSET_1:8;
then T is finite by YELLOW15:30;
hence contradiction by A1; :: thesis: verum