set a = the Element of L;
set r = the Relation of { the Element of L};
A1:
for x, y being Element of L st x in { the Element of L} & y in { the Element of L} & ex_sup_of {x,y},L holds
sup {x,y} in { the Element of L}
proof
let x,
y be
Element of
L;
( x in { the Element of L} & y in { the Element of L} & ex_sup_of {x,y},L implies sup {x,y} in { the Element of L} )
assume that A2:
(
x in { the Element of L} &
y in { the Element of L} )
and
ex_sup_of {x,y},
L
;
sup {x,y} in { the Element of L}
(
x = the
Element of
L &
y = the
Element of
L )
by A2, TARSKI:def 1;
then sup {x,y} =
the
Element of
L "\/" the
Element of
L
by YELLOW_0:41
.=
the
Element of
L
by YELLOW_5:1
;
hence
sup {x,y} in { the Element of L}
by TARSKI:def 1;
verum
end;
the Relation of { the Element of L} c= the InternalRel of L
then reconsider S = RelStr(# { the Element of L}, the Relation of { the Element of L} #) as strict SubRelStr of L by YELLOW_0:def 13;
take
S
; ( S is meet-inheriting & S is join-inheriting & S is strict )
for x, y being Element of L st x in { the Element of L} & y in { the Element of L} & ex_inf_of {x,y},L holds
inf {x,y} in { the Element of L}
proof
let x,
y be
Element of
L;
( x in { the Element of L} & y in { the Element of L} & ex_inf_of {x,y},L implies inf {x,y} in { the Element of L} )
assume that A7:
(
x in { the Element of L} &
y in { the Element of L} )
and
ex_inf_of {x,y},
L
;
inf {x,y} in { the Element of L}
(
x = the
Element of
L &
y = the
Element of
L )
by A7, TARSKI:def 1;
then inf {x,y} =
the
Element of
L "/\" the
Element of
L
by YELLOW_0:40
.=
the
Element of
L
by YELLOW_5:2
;
hence
inf {x,y} in { the Element of L}
by TARSKI:def 1;
verum
end;
hence
( S is meet-inheriting & S is join-inheriting & S is strict )
by A1, YELLOW_0:def 16, YELLOW_0:def 17; verum