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