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