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