begin
begin
begin
begin
definition
let L be non
empty RelStr ;
let X be
Subset of
L;
set D =
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
A1:
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } c= the
carrier of
L
correctness
coherence
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L;
by A1;
set D =
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
A2:
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } c= the
carrier of
L
correctness
coherence
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L;
by A2;
end;
begin
begin
begin
begin
:: in our terminology. It is shown bellow.