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

uparrow y c= uparrow 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

uparrow y c= uparrow x

let x be Element of L; :: thesis: for y being Element of S st x = y holds

uparrow y c= uparrow x

let y be Element of S; :: thesis: ( x = y implies uparrow y c= uparrow x )

A1: uparrow x = uparrow {x} by WAYBEL_0:def 18;

A2: uparrow y = uparrow {y} by WAYBEL_0:def 18;

assume x = y ; :: thesis: uparrow y c= uparrow x

hence uparrow y c= uparrow x by A1, A2, Th12; :: thesis: verum

for x being Element of L

for y being Element of S st x = y holds

uparrow y c= uparrow 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

uparrow y c= uparrow x

let x be Element of L; :: thesis: for y being Element of S st x = y holds

uparrow y c= uparrow x

let y be Element of S; :: thesis: ( x = y implies uparrow y c= uparrow x )

A1: uparrow x = uparrow {x} by WAYBEL_0:def 18;

A2: uparrow y = uparrow {y} by WAYBEL_0:def 18;

assume x = y ; :: thesis: uparrow y c= uparrow x

hence uparrow y c= uparrow x by A1, A2, Th12; :: thesis: verum