let L be non empty RelStr ; :: thesis: id L is infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def 32 :: thesis: id L preserves_inf_of X
assume A1: ex_inf_of X,L ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (id L) .: X,L & "/\" ((id L) .: X),L = (id L) . ("/\" X,L) )
set f = id L;
A2: (id L) .: X = X by FUNCT_1:162;
thus ex_inf_of (id L) .: X,L by A1, FUNCT_1:162; :: thesis: "/\" ((id L) .: X),L = (id L) . ("/\" X,L)
thus "/\" ((id L) .: X),L = (id L) . ("/\" X,L) by A2, FUNCT_1:35; :: thesis: verum