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 ;
for i being Element of X holds (X --> S) . i is full SubRelStr of (X --> L) . i ;
hence S |^ X is full SubRelStr of L |^ X by Th36; :: thesis: verum

end;

end;