let L1, L2 be non empty RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to YELLOW_0:def 17 :: thesis: J is join-inheriting
let x, y be Element of L2; :: according to YELLOW_0:def 17 :: thesis: ( 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 ; :: thesis: "\/" ({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; :: thesis: verum