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 )
A1: downarrow x = downarrow {x} by WAYBEL_0:def 17;
A2: downarrow y = downarrow {y} by WAYBEL_0:def 17;
assume x = y ; :: thesis: downarrow y c= downarrow x
hence downarrow y c= downarrow x by A1, A2, Th11; :: thesis: verum