set O = TrivOrthoRelStr ;
set C = the Compl of TrivOrthoRelStr;
set S = the carrier of TrivOrthoRelStr;
the Compl of TrivOrthoRelStr QuasiOrthoComplement_on TrivOrthoRelStr
proof
reconsider f = the
Compl of
TrivOrthoRelStr as
Function of
TrivOrthoRelStr,
TrivOrthoRelStr ;
A1:
for
x being
Element of the
carrier of
TrivOrthoRelStr holds
{x,(op1 . x)} = {x}
by Lm2, PARTIT_2:19, ENUMSET1:29;
for
x being
Element of
TrivOrthoRelStr holds
(
sup {x,(f . x)} = x &
inf {x,(f . x)} = x &
ex_sup_of {x,(f . x)},
TrivOrthoRelStr &
ex_inf_of {x,(f . x)},
TrivOrthoRelStr )
proof
let a be
Element of
TrivOrthoRelStr;
( sup {a,(f . a)} = a & inf {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr )
{a,(f . a)} = {a}
by A1;
hence
(
sup {a,(f . a)} = a &
inf {a,(f . a)} = a &
ex_sup_of {a,(f . a)},
TrivOrthoRelStr &
ex_inf_of {a,(f . a)},
TrivOrthoRelStr )
by YELLOW_0:38, YELLOW_0:39;
verum
end;
hence
the
Compl of
TrivOrthoRelStr QuasiOrthoComplement_on TrivOrthoRelStr
by Th14;
verum
end;
hence
TrivOrthoRelStr is QuasiOrthocomplemented
; verum