let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L
for x being Element of S holds x is Element of L
let S be non empty SubRelStr of L; :: thesis: for x being Element of S holds x is Element of L
let x be Element of S; :: thesis: x is Element of L
( x in the carrier of S & the carrier of S c= the carrier of L ) by Def13;
hence x is Element of L ; :: thesis: verum