set A = the non empty trivial set ;
set T = pcs-total the non empty trivial set ;
for x, y being Element of (pcs-total the non empty trivial set ) ex z being Element of (pcs-total the non empty trivial set ) st
( x <= z & y <= z & ( for z9 being Element of (pcs-total the non empty trivial set ) st x <= z9 & y <= z9 holds
z <= z9 ) )

proof

let x, y be Element of (pcs-total the non empty trivial set ); :: thesis: ex z being Element of (pcs-total the non empty trivial set ) st
( x <= z & y <= z & ( for z9 being Element of (pcs-total the non empty trivial set ) st x <= z9 & y <= z9 holds
z <= z9 ) )
pcs-total the non empty trivial set is trivial ;
then T0: x = y by STRUCT_0:def 10;
ex z being Element of (pcs-total the non empty trivial set ) st
( x <= z & y <= z & ( for z9 being Element of (pcs-total the non empty trivial set ) st x <= z9 & y <= z9 holds
z <= z9 ) )

proof

take z = x; :: thesis: ( x <= z & y <= z & ( for z9 being Element of (pcs-total the non empty trivial set ) st x <= z9 & y <= z9 holds
z <= z9 ) )
thus ( x <= z & y <= z ) by T0; :: thesis: for z9 being Element of (pcs-total the non empty trivial set ) st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of (pcs-total the non empty trivial set ); :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume ( x <= z9 & y <= z9 ) ; :: thesis: z <= z9
hence z <= z9 ; :: thesis: verum

end;

hence ex z being Element of (pcs-total the non empty trivial set ) st
( x <= z & y <= z & ( for z9 being Element of (pcs-total the non empty trivial set ) st x <= z9 & y <= z9 holds
z <= z9 ) ) ; :: thesis: verum

end;

then B1: pcs-total the non empty trivial set is with_suprema by LATTICE3:def 10;
for x, y being Element of (pcs-total the non empty trivial set ) ex z being Element of (pcs-total the non empty trivial set ) st
( z <= x & z <= y & ( for z9 being Element of (pcs-total the non empty trivial set ) st z9 <= x & z9 <= y holds
z9 <= z ) )

proof

let x, y be Element of (pcs-total the non empty trivial set ); :: thesis: ex z being Element of (pcs-total the non empty trivial set ) st
( z <= x & z <= y & ( for z9 being Element of (pcs-total the non empty trivial set ) st z9 <= x & z9 <= y holds
z9 <= z ) )
pcs-total the non empty trivial set is trivial ;
then T0: x = y by STRUCT_0:def 10;
ex z being Element of (pcs-total the non empty trivial set ) st
( z <= x & z <= y & ( for z9 being Element of (pcs-total the non empty trivial set ) st z9 <= x & z9 <= y holds
z9 <= z ) )

proof

take z = x; :: thesis: ( z <= x & z <= y & ( for z9 being Element of (pcs-total the non empty trivial set ) st z9 <= x & z9 <= y holds
z9 <= z ) )
thus ( z <= x & z <= y ) by T0; :: thesis: for z9 being Element of (pcs-total the non empty trivial set ) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of (pcs-total the non empty trivial set ); :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )
assume ( z9 <= x & z9 <= y ) ; :: thesis: z9 <= z
hence z9 <= z ; :: thesis: verum

end;

hence ex z being Element of (pcs-total the non empty trivial set ) st
( z <= x & z <= y & ( for z9 being Element of (pcs-total the non empty trivial set ) st z9 <= x & z9 <= y holds
z9 <= z ) ) ; :: thesis: verum

end;

then B2: pcs-total the non empty trivial set is with_infima by LATTICE3:def 11;
pcs-total the non empty trivial set is pcs-Compatible by NablaCompat;
hence ex b₁ being WAP-Lattice st
( b₁ is pcs-Compatible & b₁ is pcs-tol-reflexive & b₁ is pcs-tol-symmetric ) by B1, B2; :: thesis: verum