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