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 A1: X = {} ; :: thesis: S |^ X is full 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 full SubRelStr of L |^ X by A2, YELLOW_6:6; :: 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 by FUNCOP_1:7;
hence (X --> S) . i is full SubRelStr of (X --> L) . i by FUNCOP_1:7; :: thesis: verum

end;

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

end;

end;