consider b being Element of L such that
A1: B = (StoneH L) . b by Th13;
consider a being Element of L such that
A2: A = (StoneH L) . a by Th13;
A \/ B = (StoneH L) . (a "\/" b) by A2, A1, Th14;
hence A \/ B is Element of StoneS L by Th13; :: thesis: verum