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
set f = id L;
assume 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) )
hence ex_inf_of (id L) .: X,L by FUNCT_1:162; :: thesis: "/\" ((id L) .: X),L = (id L) . ("/\" X,L)
(id L) .: X = X by FUNCT_1:162;
hence "/\" ((id L) .: X),L = (id L) . ("/\" X,L) by FUNCT_1:35; :: thesis: verum