let L be non empty RelStr ; :: thesis: for S being non empty full SubRelStr of L
for X being set holds S |^ X is full SubRelStr of L |^ X
let S be non empty full SubRelStr of L; :: thesis: for X being set holds S |^ X is full SubRelStr of L |^ X
let X be set ; :: thesis: S |^ X is full SubRelStr of L |^ X

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: S |^ X is full SubRelStr of L |^ X

then ( S |^ X = RelStr(# {{} },(id {{} }) #) & L |^ X = RelStr(# {{} },(id {{} }) #) ) by YELLOW_1:27;
hence S |^ X is full SubRelStr of L |^ X by YELLOW_6:15; :: thesis: verum

end;

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

then reconsider X = X as non empty set ;

now

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

end;

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

end;

end;