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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

the Relation of { the Element of L} c= the InternalRel of L

proof

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

end;

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 ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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; :: 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