let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
downarrow y c= downarrow x
let S be non empty SubRelStr of L; :: thesis: for x being Element of L
for y being Element of S st x = y holds
downarrow y c= downarrow x
let x be Element of L; :: thesis: for y being Element of S st x = y holds
downarrow y c= downarrow x
let y be Element of S; :: thesis: ( x = y implies downarrow y c= downarrow x )
assume A1: x = y ; :: thesis: downarrow y c= downarrow x
( downarrow x = downarrow {x} & downarrow y = downarrow {y} ) by WAYBEL_0:def 17;
hence downarrow y c= downarrow x by A1, Th11; :: thesis: verum