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