set O = TrivOrthoRelStr ;
set C = the Compl of TrivOrthoRelStr;
set S = the carrier of TrivOrthoRelStr;
reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ;
f OrthoComplement_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;
A2:
for
x being
Element of
TrivOrthoRelStr holds
(
ex_sup_of {x,(f . x)},
TrivOrthoRelStr &
ex_inf_of {x,(f . x)},
TrivOrthoRelStr &
sup {x,(f . x)} = x &
inf {x,(f . x)} = x )
proof
let a be
Element of
TrivOrthoRelStr;
( ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr & sup {a,(f . a)} = a & inf {a,(f . a)} = a )
{a,(f . a)} = {a}
by A1;
hence
(
ex_sup_of {a,(f . a)},
TrivOrthoRelStr &
ex_inf_of {a,(f . a)},
TrivOrthoRelStr &
sup {a,(f . a)} = a &
inf {a,(f . a)} = a )
by YELLOW_0:38, YELLOW_0:39;
verum
end;
A3:
for
x being
Element of
TrivOrthoRelStr holds
(
sup {x,(f . x)} in {x,(f . x)} &
inf {x,(f . x)} in {x,(f . x)} )
proof
let a be
Element of
TrivOrthoRelStr;
( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} in {a,(f . a)} )
(
sup {a,(f . a)} = a &
inf {a,(f . a)} = a )
by A2;
hence
(
sup {a,(f . a)} in {a,(f . a)} &
inf {a,(f . a)} in {a,(f . a)} )
by TARSKI:def 2;
verum
end;
A4:
for
x being
Element of
TrivOrthoRelStr holds
(
x is_maximum_of {x,(f . x)} &
x is_minimum_of {x,(f . x)} )
proof
let a be
Element of
TrivOrthoRelStr;
( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} )
A5:
(
sup {a,(f . a)} = a &
ex_sup_of {a,(f . a)},
TrivOrthoRelStr )
by A2;
(
sup {a,(f . a)} in {a,(f . a)} &
inf {a,(f . a)} = a )
by A2, A3;
hence
(
a is_maximum_of {a,(f . a)} &
a is_minimum_of {a,(f . a)} )
by A5, A2, WAYBEL_1:def 6, WAYBEL_1:def 7;
verum
end;
for
y being
Element of
TrivOrthoRelStr holds
(
sup {y,(f . y)} is_maximum_of the
carrier of
TrivOrthoRelStr &
inf {y,(f . y)} is_minimum_of the
carrier of
TrivOrthoRelStr )
hence
f OrthoComplement_on TrivOrthoRelStr
by A2, Th14;
verum
end;
hence
TrivOrthoRelStr is Orthocomplemented
; verum