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

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