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

downarrow Y c= downarrow 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

downarrow Y c= downarrow X

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

downarrow Y c= downarrow X

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

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

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

assume A2: x in downarrow Y ; :: thesis: x in downarrow 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 15;

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

y2 >= x2 by A3, YELLOW_0:59;

hence x in downarrow X by A1, A4, WAYBEL_0:def 15; :: thesis: verum

for X being Subset of L

for Y being Subset of S st X = Y holds

downarrow Y c= downarrow 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

downarrow Y c= downarrow X

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

downarrow Y c= downarrow X

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

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

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

assume A2: x in downarrow Y ; :: thesis: x in downarrow 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 15;

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

y2 >= x2 by A3, YELLOW_0:59;

hence x in downarrow X by A1, A4, WAYBEL_0:def 15; :: thesis: verum