let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L
for X being set holds S |^ X is SubRelStr of L |^ X
let S be non empty SubRelStr of L; :: thesis: for X being set holds S |^ X is SubRelStr of L |^ X
let X be set ; :: thesis: S |^ X is SubRelStr of L |^ X
per cases ( X = {} or X <> {} ) ;
suppose A1: X = {} ; :: thesis: S |^ X is SubRelStr of L |^ X
then A2: L |^ X = RelStr(# {{}},(id {{}}) #) by YELLOW_1:27;
S |^ X = RelStr(# {{}},(id {{}}) #) by A1, YELLOW_1:27;
hence S |^ X is SubRelStr of L |^ X by A2, YELLOW_6:6; :: thesis: verum
end;
suppose X <> {} ; :: thesis: S |^ X is SubRelStr of L |^ X
then reconsider X = X as non empty set ;
for i being Element of X holds (X --> S) . i is SubRelStr of (X --> L) . i ;
hence S |^ X is SubRelStr of L |^ X by Th35; :: thesis: verum
end;
end;