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:92; :: thesis: "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L))
(id L) .: X = X by FUNCT_1:92;
hence "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) ; :: thesis: verum