let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

let S be non empty SubRelStr of L; :: thesis: for X being Subset of L

for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

let X be Subset of L; :: thesis: for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

let Y be Subset of S; :: thesis: ( X = Y implies uparrow Y c= uparrow X )

assume A1: X = Y ; :: thesis: uparrow Y c= uparrow X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow Y or x in uparrow X )

assume A2: x in uparrow Y ; :: thesis: x in uparrow X

then reconsider x1 = x as Element of S ;

consider y1 being Element of S such that

A3: y1 <= x1 and

A4: y1 in Y by A2, WAYBEL_0:def 16;

reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;

y2 <= x2 by A3, YELLOW_0:59;

hence x in uparrow X by A1, A4, WAYBEL_0:def 16; :: thesis: verum

for X being Subset of L

for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

let S be non empty SubRelStr of L; :: thesis: for X being Subset of L

for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

let X be Subset of L; :: thesis: for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

let Y be Subset of S; :: thesis: ( X = Y implies uparrow Y c= uparrow X )

assume A1: X = Y ; :: thesis: uparrow Y c= uparrow X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow Y or x in uparrow X )

assume A2: x in uparrow Y ; :: thesis: x in uparrow X

then reconsider x1 = x as Element of S ;

consider y1 being Element of S such that

A3: y1 <= x1 and

A4: y1 in Y by A2, WAYBEL_0:def 16;

reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;

y2 <= x2 by A3, YELLOW_0:59;

hence x in uparrow X by A1, A4, WAYBEL_0:def 16; :: thesis: verum