{} in {{}} by TARSKI:def 1;
then reconsider D = {{}} as non empty set ;
reconsider iD = id D as Relation of D ;
reconsider nD = nabla D as Relation of D ;
set P = pcs-Str(# D,iD,nD #);
AA: for x, y being Element of pcs-Str(# D,iD,nD #) holds x (--) y

proof

let x, y be Element of pcs-Str(# D,iD,nD #); :: thesis: x (--) y
[x,y] in [:D,D:] by ZFMISC_1:87;
then [x,y] in nabla D by EQREL_1:def 1;
hence x (--) y by PCS_0:def 7; :: thesis: verum

end;

A1: pcs-Str(# D,iD,nD #) is trivial ;
B1: the InternalRel of pcs-Str(# D,iD,nD #) is_reflexive_in the carrier of pcs-Str(# D,iD,nD #) by EQREL_1:2;
field (id D) = D by PARTIT_2:18;
then field the InternalRel of pcs-Str(# D,iD,nD #) = the carrier of pcs-Str(# D,iD,nD #) ;
then B3: the InternalRel of pcs-Str(# D,iD,nD #) is_antisymmetric_in the carrier of pcs-Str(# D,iD,nD #) by RELAT_2:def 12;
for x, y being Element of pcs-Str(# D,iD,nD #) ex z being Element of pcs-Str(# D,iD,nD #) st
( x <= z & y <= z & ( for z9 being Element of pcs-Str(# D,iD,nD #) st x <= z9 & y <= z9 holds
z <= z9 ) )

proof

let x, y be Element of pcs-Str(# D,iD,nD #); :: thesis: ex z being Element of pcs-Str(# D,iD,nD #) st
( x <= z & y <= z & ( for z9 being Element of pcs-Str(# D,iD,nD #) st x <= z9 & y <= z9 holds
z <= z9 ) )
reconsider z = {} as Element of pcs-Str(# D,iD,nD #) by TARSKI:def 1;
take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of pcs-Str(# D,iD,nD #) st x <= z9 & y <= z9 holds
z <= z9 ) )
B4: ( x = z & y = z ) by A1, STRUCT_0:def 10;
then ( [x,z] in id D & [y,z] in id D ) by RELAT_1:def 10;
then ( [x,z] in the InternalRel of pcs-Str(# D,iD,nD #) & [y,z] in the InternalRel of pcs-Str(# D,iD,nD #) ) ;
hence ( x <= z & y <= z & ( for z9 being Element of pcs-Str(# D,iD,nD #) st x <= z9 & y <= z9 holds
z <= z9 ) ) by B4, ORDERS_2:def 5; :: thesis: verum

end;

then B4: pcs-Str(# D,iD,nD #) is with_suprema by LATTICE3:def 10;
for x, y being Element of pcs-Str(# D,iD,nD #) ex z being Element of pcs-Str(# D,iD,nD #) st
( z <= x & z <= y & ( for z9 being Element of pcs-Str(# D,iD,nD #) st z9 <= x & z9 <= y holds
z9 <= z ) )

proof

let x, y be Element of pcs-Str(# D,iD,nD #); :: thesis: ex z being Element of pcs-Str(# D,iD,nD #) st
( z <= x & z <= y & ( for z9 being Element of pcs-Str(# D,iD,nD #) st z9 <= x & z9 <= y holds
z9 <= z ) )
reconsider z = {} as Element of pcs-Str(# D,iD,nD #) by TARSKI:def 1;
take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of pcs-Str(# D,iD,nD #) st z9 <= x & z9 <= y holds
z9 <= z ) )
B4: ( x = z & y = z ) by A1, STRUCT_0:def 10;
then ( [x,z] in id D & [y,z] in id D ) by RELAT_1:def 10;
hence ( z <= x & z <= y & ( for z9 being Element of pcs-Str(# D,iD,nD #) st z9 <= x & z9 <= y holds
z9 <= z ) ) by B4, ORDERS_2:def 5; :: thesis: verum

end;

then pcs-Str(# D,iD,nD #) is with_infima by LATTICE3:def 11;
then ( pcs-Str(# D,iD,nD #) is reflexive & pcs-Str(# D,iD,nD #) is antisymmetric & pcs-Str(# D,iD,nD #) is with_suprema & pcs-Str(# D,iD,nD #) is with_infima ) by B1, B3, B4, ORDERS_2:def 2, ORDERS_2:def 4;
then reconsider P = pcs-Str(# D,iD,nD #) as WAP-Lattice ;
take P ; :: thesis: ( P is trivial & P is total & P is pcs-Compatible )
thus ( P is trivial & P is total & P is pcs-Compatible ) by AA; :: thesis: verum