set L = BoolePoset 1;
consider T being Scott TopAugmentation of BoolePoset 1;
take T ; :: thesis: ( not T is trivial & T is complete & T is Scott )
( BoolePoset 1 = InclPoset (bool 1) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of (BoolePoset 1),the InternalRel of (BoolePoset 1) #) ) by YELLOW_1:4, YELLOW_9:def 4;
then A1: the carrier of T = bool 1 by YELLOW_1:1;
( 0 in {0 ,1} & 1 in {0 ,1} ) by TARSKI:def 2;
hence ( not T is trivial & T is complete & T is Scott ) by A1, STRUCT_0:def 10, YELLOW14:1; :: thesis: verum