set L = RelStr(# {T},(id {T}) #);
A1: T in QuasiTypes C by Def43;
then {T} c= QuasiTypes C by ZFMISC_1:31;
then reconsider f = (vars-function C) | {T} as Function of RelStr(# {T},(id {T}) #),VarPoset by FUNCT_2:32;
take C ; :: according to ABCMIZ_1:def 53 :: thesis: ex f being Function of RelStr(# {T},(id {T}) #),VarPoset st
( the carrier of RelStr(# {T},(id {T}) #) c= QuasiTypes C & f = (vars-function C) | the carrier of RelStr(# {T},(id {T}) #) & ( for x, y being Element of RelStr(# {T},(id {T}) #) holds f preserves_sup_of {x,y} ) )
take f ; :: thesis: ( the carrier of RelStr(# {T},(id {T}) #) c= QuasiTypes C & f = (vars-function C) | the carrier of RelStr(# {T},(id {T}) #) & ( for x, y being Element of RelStr(# {T},(id {T}) #) holds f preserves_sup_of {x,y} ) )
thus the carrier of RelStr(# {T},(id {T}) #) c= QuasiTypes C by A1, ZFMISC_1:31; :: thesis: ( f = (vars-function C) | the carrier of RelStr(# {T},(id {T}) #) & ( for x, y being Element of RelStr(# {T},(id {T}) #) holds f preserves_sup_of {x,y} ) )
thus f = (vars-function C) | the carrier of RelStr(# {T},(id {T}) #) ; :: thesis: for x, y being Element of RelStr(# {T},(id {T}) #) holds f preserves_sup_of {x,y}
let x, y be Element of RelStr(# {T},(id {T}) #); :: thesis: f preserves_sup_of {x,y}
set F = {x,y};
assume ex_sup_of {x,y}, RelStr(# {T},(id {T}) #) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: {x,y}, VarPoset & "\/" ((f .: {x,y}),VarPoset) = f . ("\/" ({x,y},RelStr(# {T},(id {T}) #))) )
A2: x = T by TARSKI:def 1;
y = T by TARSKI:def 1;
then A3: {x,y} = {T} by A2, ENUMSET1:29;
dom f = {T} by FUNCT_2:def 1;
then A4: Im (f,T) = {(f . x)} by A2, FUNCT_1:59;
hence ex_sup_of f .: {x,y}, VarPoset by A3, YELLOW_0:38; :: thesis: "\/" ((f .: {x,y}),VarPoset) = f . ("\/" ({x,y},RelStr(# {T},(id {T}) #)))
thus sup (f .: {x,y}) = f . x by A3, A4, YELLOW_0:39
.= f . (sup {x,y}) by A2, TARSKI:def 1 ; :: thesis: verum