consider a being Element of L;
consider r being Relation of {a};
A1: for x, y being Element of L st x in {a} & y in {a} & ex_sup_of {x,y},L holds
sup {x,y} in {a}

proof

let x, y be Element of L; :: thesis: ( x in {a} & y in {a} & ex_sup_of {x,y},L implies sup {x,y} in {a} )
assume that
A2: ( x in {a} & y in {a} ) and
ex_sup_of {x,y},L ; :: thesis: sup {x,y} in {a}
( x = a & y = a ) by A2, TARSKI:def 1;
then sup {x,y} = a "\/" a by YELLOW_0:41
.= a by YELLOW_5:1 ;
hence sup {x,y} in {a} by TARSKI:def 1; :: thesis: verum

end;

r c= the InternalRel of L

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in r or z in the InternalRel of L )
assume z in r ; :: thesis: z in the InternalRel of L
then consider x, y being set such that
A3: z = [x,y] and
A4: x in {a} and
A5: y in {a} by RELSET_1:6;
x = a by A4, TARSKI:def 1;
then A6: z = [a,a] by A3, A5, TARSKI:def 1;
a <= a ;
hence z in the InternalRel of L by A6, ORDERS_2:def 9; :: thesis: verum

end;

then reconsider S = RelStr(# {a},r #) as strict SubRelStr of L by YELLOW_0:def 13;
take S ; :: thesis: ( S is meet-inheriting & S is join-inheriting & S is strict )
for x, y being Element of L st x in {a} & y in {a} & ex_inf_of {x,y},L holds
inf {x,y} in {a}

proof

let x, y be Element of L; :: thesis: ( x in {a} & y in {a} & ex_inf_of {x,y},L implies inf {x,y} in {a} )
assume that
A7: ( x in {a} & y in {a} ) and
ex_inf_of {x,y},L ; :: thesis: inf {x,y} in {a}
( x = a & y = a ) by A7, TARSKI:def 1;
then inf {x,y} = a "/\" a by YELLOW_0:40
.= a by YELLOW_5:2 ;
hence inf {x,y} in {a} by TARSKI:def 1; :: thesis: verum

end;

hence ( S is meet-inheriting & S is join-inheriting & S is strict ) by A1, YELLOW_0:def 16, YELLOW_0:def 17; :: thesis: verum