let L1, L2 be non empty RelStr ; for A being SubRelStr of L1
for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting holds
J is join-inheriting
let A be SubRelStr of L1; for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting holds
J is join-inheriting
let J be SubRelStr of L2; ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting implies J is join-inheriting )
assume that
A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #)
and
A2:
RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #)
and
A3:
for x, y being Element of L1 st x in the carrier of A & y in the carrier of A & ex_sup_of {x,y},L1 holds
sup {x,y} in the carrier of A
; YELLOW_0:def 17 J is join-inheriting
let x, y be Element of L2; YELLOW_0:def 17 ( not x in the carrier of J or not y in the carrier of J or not ex_sup_of {x,y},L2 or "\/" ({x,y},L2) in the carrier of J )
assume that
A4:
( x in the carrier of J & y in the carrier of J )
and
A5:
ex_sup_of {x,y},L2
; "\/" ({x,y},L2) in the carrier of J
reconsider x1 = x, y1 = y as Element of L1 by A1;
sup {x1,y1} in the carrier of A
by A1, A2, A3, A4, A5, YELLOW_0:14;
hence
"\/" ({x,y},L2) in the carrier of J
by A1, A2, A5, YELLOW_0:26; verum