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:15; :: thesis: verum

end;

suppose X <> {} ; :: thesis: S |^ X is SubRelStr of L |^ X

then reconsider X = X as non empty set ;

now

let i be Element of X; :: thesis: (X --> S) . i is SubRelStr of (X --> L) . i
(X --> L) . i = L by FUNCOP_1:13;
hence (X --> S) . i is SubRelStr of (X --> L) . i by FUNCOP_1:13; :: thesis: verum

end;

hence S |^ X is SubRelStr of L |^ X by Th38; :: thesis: verum

end;

end;